diff options
| -rwxr-xr-x | configure | 5 | ||||
| -rw-r--r-- | lib/compat.ml4 | 16 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 2 | ||||
| -rw-r--r-- | parsing/vernacextend.ml4 | 2 |
5 files changed, 16 insertions, 11 deletions
@@ -531,11 +531,6 @@ if [ "$usecamlp5" = "yes" ]; then fi camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` - if [ "`$camlp4oexec -pmode 2>&1`" != "transitional" ]; then - echo "Error: $camlp4oexec not found, or not in transitional mode!" - echo "Configuration script failed!" - exit 1 - fi case `$camlp4oexec -v 2>&1` in *4.0*|*5.00*) echo "Camlp5 version < 5.01 not supported." diff --git a/lib/compat.ml4 b/lib/compat.ml4 index d3f28b057..8d8483b49 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -185,12 +185,22 @@ let maybe_curry f = f let maybe_uncurry f = f END +(** Compatibility with camlp5 strict mode *) +IFDEF CAMLP5 THEN + IFDEF STRICT THEN + let vala x = Ploc.VaVal x + ELSE + let vala x = x + END +ELSE + let vala x = x +END (** Fix a quotation difference in [str_item] *) let declare_str_items loc l = IFDEF CAMLP5 THEN - MLast.StDcl (loc,l) (* correspond to <:str_item< declare $list:l'$ end >> *) + MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *) ELSE Ast.stSem_of_list l END @@ -198,13 +208,13 @@ END (** Quotation difference for match clauses *) let default_patt loc = - (<:patt< _ >>, None, <:expr< failwith "Extension: cannot occur" >>) + (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>) IFDEF CAMLP5 THEN let make_fun loc cl = let l = cl @ [default_patt loc] in - MLast.ExFun (loc,l) (* correspond to <:expr< fun [ $list:l$ ] >> *) + MLast.ExFun (loc, vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) ELSE diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index d5ffa6457..eceb02d53 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 e1ae91966..ec305ee2e 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 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 = |