From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Jun 2005 14:31:43 +0000 (+0000)
Subject: The user is no longer obliged to give the types for definitions.
X-Git-Tag: PRE_STORAGE~77
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c347684900a4e2b17a6c1d372fb142bebd8cd250;p=helm.git

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 9f65555a4..4b94226cb 100644
--- 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 =