From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 16:50:36 +0000 (+0000)
Subject: The type of a top-level "let rec" can be optional.
X-Git-Tag: PRE_INDEX_1~25
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e42e345f711e051c903072d8cd994ab7b2154b25;p=helm.git

The type of a top-level "let rec" can be optional.
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index e267aff6a..9f65555a4 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -553,8 +553,7 @@ EXTEND
           let name,ty = 
             match defs with
             | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
-            | ((Cic.Name name,None),_,_) :: _ -> 
-                fail loc ("No type given for " ^ name)
+            | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
             | _ -> assert false 
           in
           let body = CicAst.Ident (name,None) in