Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-08-06 20:48:49 -0700 (Thu, 06 Aug 1998)
Revision: 2421
Log message:
Removed "ugly" sequents.
Term_base_ds: now dest_term will raise Invalid_argument
when called on a sequent term
Simple_print: I wrote some temporary code for printing sequents,
but it should definitely be rewritten
Changes | Path |
+57 -0 | metaprl/refiner/reflib/simple_print.ml |
+2 -48 | metaprl/refiner/term_ds/term_base_ds.mlp |