From 30410fbb67dca41b66f98e5453627fb8071d2cbc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Oct 2004 10:13:21 +0000
Subject: Réinstallation des lieurs avant l'énoncé de Theorem/Lemma (non
 documenté mais utilisé !)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6206 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b653654589..fbfd35863e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -189,8 +189,8 @@ GEXTEND Gram
   ;
   gallina:
     (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; ":"; c = constr ->
-         VernacStartTheoremProof (thm, id, ([], c), false, (fun _ _ -> ()))
+    [ [ thm = thm_token; id = identref; bl = binders_list; ":"; c = constr ->
+         VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
       | (f,d) = def_token; id = identref; b = def_body -> 
           VernacDefinition (d, id, b, f)
       | stre = assumption_token; bl = ne_params_list -> 
-- 
cgit v1.2.3