Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-25 01:49:28 -0700 (Wed, 25 May 2005)
Revision: 7327
Log message:

      Numerous documentation fixes:
      
       - MP_DEBUG=spell fixes (MP_DEBUG=spell finally compiles again)
      
       - Now docoff/junk/docon sequence does not introduce empty vertical space
      
       - Removed the old reflection theories from the theories.pdf, replacing them
         with the new itt_hoas_* theories.
      
       - Chaged so that any TeX printout of a module always starts in the "docoff"
         mode. This makes it unnecessary to always terminate documented modules in
         the "docoff" mode.
      

Changes  Path
+4 -0 metaprl/lib/words
+13 -6 metaprl/support/display/comment.ml
+1 -0 metaprl/support/display/comment.mli
+1 -1 metaprl/theories/base/OMakefile
+13 -13 metaprl/theories/base/base_reflection.ml
+6 -5 metaprl/theories/itt/OMakefile
+1 -1 metaprl/theories/itt/itt_closure.ml
+2 -3 metaprl/theories/itt/itt_esquash.ml
+2 -1 metaprl/theories/itt/itt_functions.ml
+5 -5 metaprl/theories/itt/itt_hoas_base.ml
+5 -5 metaprl/theories/itt/itt_hoas_debruijn.ml
+1 -1 metaprl/theories/itt/itt_hoas_debruijn.mli
Added metaprl/theories/itt/itt_hoas_destterm.ml
Properties metaprl/theories/itt/itt_hoas_destterm.ml
Added metaprl/theories/itt/itt_hoas_destterm.mli
Properties metaprl/theories/itt/itt_hoas_destterm.mli
+1 -1 metaprl/theories/itt/itt_hoas_operator.ml
+2 -2 metaprl/theories/itt/itt_hoas_vector.ml
+2 -2 metaprl/theories/itt/itt_record_exm.ml
+6 -7 metaprl/theories/itt/itt_reflection_new.ml
+2 -2 metaprl/theories/itt/itt_synt_bterm.ml
+2 -1 metaprl/theories/itt/itt_synt_lang.ml
+10 -7 metaprl/theories/itt/itt_synt_subst.ml
+3 -3 metaprl/theories/itt/itt_synt_var.ml
+2 -2 metaprl/theories/itt/itt_union.ml
+8 -1 texinputs/metaprl.tex