diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-25 20:53:24 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-25 20:53:24 +0000 |
| commit | bc2cebecc14bee4a1a486ff0bead87b6fd69d452 (patch) | |
| tree | 69c068ce087a768c3e5d6a364d9af004df9976be /parsing/vernacextend.ml4 | |
| parent | 5d39716249aff66eff1d710e6222901b111b0637 (diff) | |
Fix compilation with camlp5 (Closes: #2487)
With hints from Daniel de Rauglaudre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/vernacextend.ml4')
| -rw-r--r-- | parsing/vernacextend.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 58946eda9..cc3bd07e8 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -36,7 +36,7 @@ let check_unicity s l = let make_clause (_,pt,e) = (make_patt pt, - Some (make_when (MLast.loc_of_expr e) pt), + vala (Some (make_when (MLast.loc_of_expr e) pt)), make_let e pt) let make_fun_clauses loc s l = |