/[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 2494 by jyh, Tue Oct 13 01:14:08 1998 UTC revision 2502 by nogin, Tue Oct 13 09:01:06 1998 UTC
# Line 187  Line 187 
187   * Right now most things are not supported.   * Right now most things are not supported.
188   *)   *)
189  let not_supported loc str =  let not_supported loc str =
190     Stdpp.raise_with_loc loc (RefineError ("nltop", StringStringError ("operation is not implemented", str)))     Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
191    
192  let type_error loc str =  let type_error loc str =
193     Stdpp.raise_with_loc loc (RefineError ("type error", StringError str))     Stdpp.raise_with_loc loc (RefineError ("type error", StringError str))

Legend:
Removed from v.2494  
changed lines
  Added in v.2502

  ViewVC Help
Powered by ViewVC 1.1.26