Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-19 11:26:36 -0800 (Wed, 19 Jan 2005)
Revision: 6442
Log message:

      Global update to use token opnames instead of strings.
      The theories that use records will get a lot of warning like this:
      
         warning: undeclared token: car
      
      To fix this, you need to declare the term 'car'.
      For most of labels, declaring them will be sufficient.
      For car, there are two places in the code that look like this:
      
         let car_opname = mk_opname "car" nil_opname
      
      Once you decide where to declare the opname, you should put this
      there.
      
         let car_opname = opname_of_term << car >>
      

Changes  Path
+17 -0 metaprl-branches/opname_classes/filter/filter/filter_parse.ml
+29 -17 metaprl-branches/opname_classes/filter/filter/term_grammar.ml
+2 -2 metaprl-branches/opname_classes/theories/czf/czf_itt_equiv.ml
+3 -9 metaprl-branches/opname_classes/theories/czf/czf_itt_equiv.mli
+1 -5 metaprl-branches/opname_classes/theories/czf/czf_itt_sall.mli
+1 -5 metaprl-branches/opname_classes/theories/czf/czf_itt_sexists.mli
+3 -3 metaprl-branches/opname_classes/theories/experimental/compile/m_ast.ml
+1 -1 metaprl-branches/opname_classes/theories/experimental/compile/m_ast.mli
+4 -4 metaprl-branches/opname_classes/theories/experimental/compile/m_cps.ml
+1 -1 metaprl-branches/opname_classes/theories/experimental/compile/m_doc_ir.ml
+1 -1 metaprl-branches/opname_classes/theories/experimental/compile/m_doc_ir.mli
+2 -2 metaprl-branches/opname_classes/theories/experimental/compile/m_doc_proposal.ml
+1 -1 metaprl-branches/opname_classes/theories/experimental/compile/m_doc_proposal.mli
+3 -3 metaprl-branches/opname_classes/theories/experimental/compile/m_ir.ml
+1 -1 metaprl-branches/opname_classes/theories/experimental/compile/m_ir.mli
+5 -5 metaprl-branches/opname_classes/theories/experimental/compile/m_ir_ast.ml
+10 -8 metaprl-branches/opname_classes/theories/experimental/compile/m_test.ml
+12 -12 metaprl-branches/opname_classes/theories/experimental/compile/m_x86_asm.ml
+4 -4 metaprl-branches/opname_classes/theories/experimental/compile/m_x86_asm.mli
+12 -12 metaprl-branches/opname_classes/theories/experimental/compile/m_x86_codegen.ml
+11 -11 metaprl-branches/opname_classes/theories/experimental/compile/m_x86_term.ml
+3 -0 metaprl-branches/opname_classes/theories/experimental/syntax/OMakefile
+5 -2 metaprl-branches/opname_classes/theories/experimental/syntax/syntax_test.ml
+1 -2 metaprl-branches/opname_classes/theories/itt/itt_algebra_df.ml
+1 -5 metaprl-branches/opname_classes/theories/itt/itt_atom.ml
+2 -2 metaprl-branches/opname_classes/theories/itt/itt_atom.mli
+4 -3 metaprl-branches/opname_classes/theories/itt/itt_grouplikeobj.ml
+2 -2 metaprl-branches/opname_classes/theories/itt/itt_record.mli
+5 -3 metaprl-branches/opname_classes/theories/itt/itt_ring2.ml