diff options
| author | glondu | 2011-01-25 20:53:24 +0000 |
|---|---|---|
| committer | glondu | 2011-01-25 20:53:24 +0000 |
| commit | bc2cebecc14bee4a1a486ff0bead87b6fd69d452 (patch) | |
| tree | 69c068ce087a768c3e5d6a364d9af004df9976be /parsing | |
| 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')
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 2 | ||||
| -rw-r--r-- | parsing/vernacextend.ml4 | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index d5ffa6457f..eceb02d53e 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -506,7 +506,7 @@ let rec patt_of_expr e = match e with | ExAcc (_, e1, e2) -> PaAcc (loc, patt_of_expr e1, patt_of_expr e2) | ExApp (_, e1, e2) -> PaApp (loc, patt_of_expr e1, patt_of_expr e2) - | ExLid (_, "loc") -> PaAny loc + | ExLid (_, x) when x = vala "loc" -> PaAny loc | ExLid (_, s) -> PaLid (loc, s) | ExUid (_, s) -> PaUid (loc, s) | ExStr (_, s) -> PaStr (loc, s) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index e1ae919663..ec305ee2eb 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -59,7 +59,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 = diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 58946eda9a..cc3bd07e8a 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 = |