From 1f951ff0d587130039d425d8892a41d8126befd0 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 12 Oct 2004 10:13:28 +0000 Subject: Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs sont autorisés avant l'énoncé MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6207 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_vernacnew.ml4 | 3 +-- translate/ppvernacnew.ml | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 29985d867..def78d92a 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -93,9 +93,8 @@ GEXTEND Gram gallina: (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = identref; (* bl = LIST0 binder; *) ":"; + [ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":"; c = lconstr -> - let bl = [] in VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ())) | (f,d) = def_token; id = identref; b = def_body -> VernacDefinition (d, id, b, f) diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index f4dce4cf0..085dcccb1 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -622,7 +622,7 @@ let rec pr_vernac = function hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++ (match bl with | [] -> mt() - | _ -> error "Statements with local binders no longer supported") + | _ -> pr_binders bl ++ spc()) ++ str":" ++ pr_spc_type (rename_bound_variables (snd id) c)) | VernacEndProof Admitted -> str"Admitted" | VernacEndProof (Proved (opac,o)) -> (match o with -- cgit v1.2.3