The user is no longer obliged to give the types for definitions.

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9f65555a4e80c8dc999fad607b484d55df5ef9cb..4b94226cbe2ae63f2c94ee85eb12d85ed9dfaa4d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -548,6 +548,9 @@ EXTEND
     | flavour = theorem_flavour; name = OPT 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;
+      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+        TacticAst.Theorem (loc, flavour, name, CicAst.Implicit, body)
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = let_defs -> 
           let name,ty =