/[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 2859 by nogin, Mon Nov 22 05:43:56 1999 UTC revision 2911 by jyh, Thu Feb 24 01:42:53 2000 UTC
# Line 33  Line 33 
33  open MLast  open MLast
34    
35  open Refiner.Refiner.TermType  open Refiner.Refiner.TermType
36    open Refiner.Refiner.TermAddr
37  open Refiner.Refiner.RefineError  open Refiner.Refiner.RefineError
38  open Mp_resource  open Mp_resource
39    
# Line 329  Line 330 
330                    AddressExpr a ->                    AddressExpr a ->
331                       f a                       f a
332                  | _ ->                  | _ ->
333                       type_error loc "expr should be an address"                       f (make_address (int_list_of_list loc a))
334              end              end
335    
336         | AddrFunExpr f ->         | AddrFunExpr f ->

Legend:
Removed from v.2859  
changed lines
  Added in v.2911

  ViewVC Help
Powered by ViewVC 1.1.26