diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-12 10:13:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-12 10:13:21 +0000 |
| commit | 30410fbb67dca41b66f98e5453627fb8071d2cbc (patch) | |
| tree | c24719e5766cf980f41b28693a9c9e61a53eb951 /parsing/g_vernac.ml4 | |
| parent | 170e88817206ada3812d2fc973f4423dda113f04 (diff) | |
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
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b65365458..fbfd35863 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 -> |