/[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 2772 by nogin, Sun Jul 4 00:42:06 1999 UTC revision 2811 by jyh, Fri Sep 3 23:41:50 1999 UTC
# Line 55  Line 55 
55   | TermExpr of term   | TermExpr of term
56   | TacticExpr of tactic   | TacticExpr of tactic
57   | ConvExpr of conv   | ConvExpr of conv
58     | AddressExpr of address
59    
60     (* Uptyped tuples and functions *)     (* Uptyped tuples and functions *)
61   | ListExpr of expr list   | ListExpr of expr list
# Line 70  Line 71 
71   | TacticFunExpr of (tactic -> expr)   | TacticFunExpr of (tactic -> expr)
72   | IntTacticFunExpr of ((int -> tactic) -> expr)   | IntTacticFunExpr of ((int -> tactic) -> expr)
73   | ConvFunExpr of (conv -> expr)   | ConvFunExpr of (conv -> expr)
74     | AddressFunExpr of (address -> expr)
75    
76     (* These functions take lists *)     (* These functions take lists *)
77   | AddrFunExpr of (int list -> expr)   | AddrFunExpr of (int list -> expr)
# Line 321  Line 323 
323                  | _ ->                  | _ ->
324                       type_error loc "expr should be a conversion"                       type_error loc "expr should be a conversion"
325              end              end
326           | AddressFunExpr f ->
327                begin
328                   match a with
329                      AddressExpr a ->
330                         f a
331                    | _ ->
332                         type_error loc "expr should be an address"
333                end
334    
335         | AddrFunExpr f ->         | AddrFunExpr f ->
336              f (int_list_of_list loc a)              f (int_list_of_list loc a)
# Line 339  Line 349 
349         | TermExpr _         | TermExpr _
350         | TacticExpr _         | TacticExpr _
351         | ConvExpr _         | ConvExpr _
352           | AddressExpr _
353         | ListExpr _         | ListExpr _
354         | TupleExpr _ ->         | TupleExpr _ ->
355              type_error loc "expr should be a function"              type_error loc "expr should be a function"

Legend:
Removed from v.2772  
changed lines
  Added in v.2811

  ViewVC Help
Powered by ViewVC 1.1.26