From c347684900a4e2b17a6c1d372fb142bebd8cd250 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 10 Jun 2005 14:31:43 +0000 Subject: [PATCH] The user is no longer obliged to give the types for definitions. --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 3 +++ 1 file changed, 3 insertions(+) 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> (* ≝ *); body = term -> body ] -> TacticAst.Theorem (loc, flavour, name, typ, body) + | flavour = theorem_flavour; name = OPT IDENT; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + TacticAst.Theorem (loc, flavour, name, CicAst.Implicit, body) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = let_defs -> let name,ty = -- 2.39.2