Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-25 22:35:52 -0700 (Wed, 25 Aug 2004)
Revision: 6140
Log message:

      Beofre displaying a term, convert every Context in it into a Hypothesis.
      (<H...> would become df_context{'H...} with H becoming a second-order
      variable with the same context dependencies and subterms as the original context).
      Basically, this means that we have one centralized "standard" hack for contexts
      as opposed to having to reimplement it in every theory that wants non-default
      display forms for sequents.
      

Changes	Path
+10 -1	metaprl/refiner/term_gen/term_meta_gen.ml
+18 -20	metaprl/support/display/base_dform.ml
+5 -0	metaprl/support/display/base_dform.mli
+2 -23	metaprl/theories/cic/cic_ind_type.ml