X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;fp=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=7522d3c792546a9e042f64aeda9cda048887a21d;hb=928af763320668168206e88d93e8a77698f3b925;hp=4894218e8fa28ad10f78c67bc6c2ba027ca055ab;hpb=c9c6cae5121a25b05450ea42578f14f74569cfbf;p=helm.git

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index 4894218e8..7522d3c79 100644
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -45,6 +45,7 @@ type ('a,'b,'c,'d,'e) grammars = {
   sym_attributes: (string option * string option) Grammar.Entry.e;
   sym_table: (string * Stdpp.location Grammar.Entry.e) list;
   let_defs: 'c Grammar.Entry.e;
+  let_codefs: 'c Grammar.Entry.e;
   protected_binder_vars: 'd Grammar.Entry.e;
   level2_meta: 'b Grammar.Entry.e;
 }
@@ -672,10 +673,11 @@ END
   let term = grammars.term in
   let atag_attributes = grammars.sym_attributes in
   let let_defs = grammars.let_defs in
+  let let_codefs = grammars.let_codefs in
   let ident = grammars.ident in
   let protected_binder_vars = grammars.protected_binder_vars in
 EXTEND
-  GLOBAL: level2_ast term let_defs protected_binder_vars ident atag_attributes;
+  GLOBAL: level2_ast term let_defs let_codefs protected_binder_vars ident atag_attributes;
   level2_ast: [ [ p = term -> p ] ];
   sort: [
     [ "Prop" -> `Prop
@@ -938,6 +940,7 @@ let initial_grammars loctable keywords =
       [] initial_symbols
   in
   let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
+  let let_codefs = Grammar.Entry.create level2_ast_grammar "let_codefs" in
   let protected_binder_vars = 
     Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
   let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in
@@ -949,6 +952,7 @@ let initial_grammars loctable keywords =
     sym_table=sym_table;
     sym_attributes=sym_attributes;
     let_defs=let_defs;
+    let_codefs=let_codefs;
     protected_binder_vars=protected_binder_vars;
     level2_meta=level2_meta;
     level2_ast_grammar=level2_ast_grammar;
@@ -1025,6 +1029,7 @@ let level2_ast_grammar status =
   status#notation_parser_db.grammars.level2_ast_grammar
 let term status = status#notation_parser_db.grammars.term
 let let_defs status = status#notation_parser_db.grammars.let_defs
+let let_codefs status = status#notation_parser_db.grammars.let_codefs
 let protected_binder_vars status = 
   status#notation_parser_db.grammars.protected_binder_vars