/[mojave]/metaprl/theories/tactic/mptop.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/mptop.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3085 by nogin, Wed Oct 18 21:32:01 2000 UTC revision 3086 by nogin, Sun Oct 22 20:58:58 2000 UTC
# Line 57  Line 57 
57    
58  open Refiner.Refiner.TermType  open Refiner.Refiner.TermType
59  open Refiner.Refiner.TermAddr  open Refiner.Refiner.TermAddr
60    open Refiner.Refiner.TermMan
61  open Refiner.Refiner.RefineError  open Refiner.Refiner.RefineError
62  open Mp_resource  open Mp_resource
63    
# Line 399  Line 400 
400                 match a with                 match a with
401                    AddressExpr a ->                    AddressExpr a ->
402                       f a                       f a
403                    | IntExpr i ->
404                         f (clause_address i)
405                  | ListExpr _ ->                  | ListExpr _ ->
406                       f (make_address (int_list_of_list loc a))                       f (make_address (int_list_of_list loc a))
407                  | _ ->                  | _ ->

Legend:
Removed from v.3085  
changed lines
  Added in v.3086

  ViewVC Help
Powered by ViewVC 1.1.26