Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-21 21:52:45 -0700 (Wed, 21 Apr 2004)
Revision: 5691
Log message:

      This commit changes the way the AutoMustComplete flag for intro annotations is
      implemented.
      
      Instead of using it to check the item found by the term table _after_ it is
      found, the AutoMustComplete flag is now checked _during_ the term table lookup.
      This means that the AutoMustComplete entries will now be completely ignored
      during the "normal" phase of autoT, allowing it to fall back to less specific
      entries. The manual entires to intro now have to include an extra boolean field
      --- setting it to true has the same effect as AutoMustComplete.
      
      P.S. The meaning and implementation of CondMustComplete did not change.
      

Changes  Path
+16 -14 metaprl/support/tactics/dtactic.ml
+4 -3 metaprl/support/tactics/dtactic.mli
+1 -1 metaprl/theories/itt/itt_esquash.ml
+11 -1 metaprl/theories/itt/itt_group.ml
+3 -2 metaprl/theories/itt/itt_int_ext.ml
+12490 -13223 metaprl/theories/itt/itt_int_ext.prla
+2 -1 metaprl/theories/itt/itt_nat.ml
+6023 -8930 metaprl/theories/itt/itt_nat.prla
+5401 -10129 metaprl/theories/itt/itt_poly.prla
+1 -1 metaprl/theories/itt/itt_quotient.ml
+3 -3 metaprl/theories/itt/itt_quotient_group.ml
+2 -2 metaprl/theories/itt/itt_rat.ml
+488 -516 metaprl/theories/itt/itt_ring2.prla
+1 -1 metaprl/theories/itt/itt_subtype.ml