From e42e345f711e051c903072d8cd994ab7b2154b25 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 16:50:36 +0000 Subject: [PATCH] The type of a top-level "let rec" can be optional. --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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 -- 2.39.2