Big commit and major code clean-up:

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index a7d43bb45f75461cda893201a49459bc458f0dda..feb161d7fe84aaa022271e5d7338b839a0f9e17b 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -553,12 +553,12 @@ EXTEND
       [ IDENT "set"    ]; n = QSTRING; v = QSTRING ->
         TacticAst.Set (loc, n, v)
     | [ IDENT "qed"   ] -> TacticAst.Qed loc
-    | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+    | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
-        TacticAst.Theorem (loc, flavour, name, typ, body)
-    | flavour = theorem_flavour; name = OPT IDENT;
+        TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))
+    | flavour = theorem_flavour; name = IDENT;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
-        TacticAst.Theorem (loc, flavour, name, CicAst.Implicit, body)
+        TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = let_defs -> 
           let name,ty = 
@@ -568,19 +568,19 @@ EXTEND
             | _ -> assert false 
           in
           let body = CicAst.Ident (name,None) in
-          TacticAst.Theorem(loc, `Definition, Some name, ty,
-            Some (CicAst.LetRec (ind_kind, defs, body)))
+          TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty,
+            Some (CicAst.LetRec (ind_kind, defs, body))))
           
     | [ IDENT "inductive" ]; spec = inductive_spec ->
         let (params, ind_types) = spec in
-        TacticAst.Inductive (loc, params, ind_types)
+        TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
     | [ IDENT "coinductive" ]; spec = inductive_spec ->
         let (params, ind_types) = spec in
         let ind_types = (* set inductive flags to false (coinductive) *)
           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
             ind_types
         in
-        TacticAst.Inductive (loc, params, ind_types)
+        TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
     | [ IDENT "coercion" ] ; name = IDENT -> 
         TacticAst.Coercion (loc, CicAst.Ident (name,Some []))
     | [ IDENT "coercion" ] ; name = URI -> 
@@ -588,7 +588,7 @@ EXTEND
     | [ IDENT "alias"   ]; spec = alias_spec ->
         TacticAst.Alias (loc, spec)
     | [ IDENT "record" ]; (params,name,ty,fields) = record_spec ->
-        TacticAst.Record (loc, params,name,ty,fields)
+        TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields))
   ]];
 
   executable: [