aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build27
-rw-r--r--parsing/argextend.ml42
-rw-r--r--parsing/q_constr.ml42
-rw-r--r--parsing/tacextend.ml42
-rw-r--r--parsing/vernacextend.ml42
-rw-r--r--tactics/extratactics.ml49
-rw-r--r--tools/compat5.ml13
-rw-r--r--tools/compat5.mlp23
-rw-r--r--tools/compat5b.ml13
-rw-r--r--tools/compat5b.mlp23
10 files changed, 108 insertions, 8 deletions
diff --git a/Makefile.build b/Makefile.build
index adba23753..0540b9a9a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -499,6 +499,20 @@ $(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml,,str unix)
+# Special rule for the compatibility-with-camlp5 extension for camlp4
+
+ifeq ($(CAMLP4),camlp4)
+tools/compat5.cmo: tools/compat5.mlp
+ $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+tools/compat5b.cmo: tools/compat5b.mlp
+ $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $<
+else
+tools/compat5.cmo: tools/compat5.ml
+ $(OCAMLC) -c $<
+tools/compat5b.cmo: tools/compat5b.ml
+ $(OCAMLC) -c $<
+endif
+
###########################################################################
# Installation
###########################################################################
@@ -673,11 +687,11 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml
toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
$(SHOW)'CAMLP4O $<'
- $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< $(TOTARGET)
+ $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@
toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
$(SHOW)'CAMLP4O $<'
- $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< $(TOTARGET)
+ $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@
# pretty printing of the revision number when compiling a checked out
# source tree
@@ -796,12 +810,17 @@ plugins/%_mod.ml: plugins/%.mllib
$(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
$(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@
-%.ml: %.ml4 | %.ml4.d
+# NB: compatibility modules for camlp4:
+# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
+# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
+# syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps
+
+%.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo
$(SHOW)'CAMLP4O $<'
$(HIDE)\
DEPS=$(CAMLP4DEPS); \
if ls $${DEPS} > /dev/null 2>&1; then \
- $(CAMLP4O) $(PR_O) -I $(CAMLLIB) $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \
+ $(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \
else echo $< : Dependency $${DEPS} not ready yet; false; fi
%.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY)
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index e156bdc26..fc1f05dad 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(*i camlp4deps: "tools/compat5b.cmo" i*)
+
open Genarg
open Q_util
open Egrammar
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index fb34a5aa2..43f455924 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(*i camlp4deps: "tools/compat5b.cmo" i*)
+
open Rawterm
open Term
open Names
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index f64c8f700..3aac36c08 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(*i camlp4deps: "tools/compat5b.cmo" i*)
+
open Util
open Genarg
open Q_util
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 1fa0e7e99..9ed89536c 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(*i camlp4deps: "tools/compat5b.cmo" i*)
+
open Util
open Genarg
open Q_util
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0ddb4da75..e71e6366c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,6 +21,7 @@ open Util
open Termops
open Evd
open Equality
+open Compat
(**********************************************************************)
(* replace, discriminate, injection, simplify_eq *)
@@ -543,7 +544,7 @@ let subst_var_with_hole occ tid t =
| RVar (_,id) as x ->
if id = tid
then (decr occref; if !occref = 0 then x
- else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))))
+ else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))))
else x
| c -> map_rawconstr_left_to_right substrec c in
let t' = substrec t
@@ -556,7 +557,7 @@ let subst_hole_with_term occ tc t =
let rec substrec = function
| RHole (_,Evd.QuestionMark(Evd.Define true)) ->
decr occref; if !occref = 0 then tc
- else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))
+ else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))
| c -> map_rawconstr_left_to_right substrec c
in
substrec t
@@ -578,8 +579,8 @@ let hResolve id c occ t gl =
try
Pretyping.Default.understand sigma env t_hole
with
- | Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
- resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole)
+ | Loc.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
+ resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
in
let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
let t_constr_type = Retyping.get_type_of env sigma t_constr in
diff --git a/tools/compat5.ml b/tools/compat5.ml
new file mode 100644
index 000000000..6a76895cd
--- /dev/null
+++ b/tools/compat5.ml
@@ -0,0 +1,13 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* This file is meant for camlp5, for which there is nothing to
+ add to gain camlp5 compatibility :-).
+
+ See [compat5.mlp] for the [camlp4] counterpart
+*)
diff --git a/tools/compat5.mlp b/tools/compat5.mlp
new file mode 100644
index 000000000..c3c7e9995
--- /dev/null
+++ b/tools/compat5.mlp
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
+ - GEXTEND ... becomes EXTEND ...
+*)
+
+open Camlp4.PreCast
+
+let rec my_token_filter = parser
+ | [< '(KEYWORD "GEXTEND", loc); s >] ->
+ [< '(KEYWORD "EXTEND", loc); my_token_filter s >]
+ | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
+ | [< >] -> [< >]
+
+let _ =
+ Token.Filter.define_filter (Gram.get_filter())
+ (fun prev strm -> prev (my_token_filter strm))
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
new file mode 100644
index 000000000..03bdb358b
--- /dev/null
+++ b/tools/compat5b.ml
@@ -0,0 +1,13 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* This file is meant for camlp5, for which there is nothing to
+ add to gain camlp5 compatibility :-).
+
+ See [compat5b.mlp] for the [camlp4] counterpart
+*)
diff --git a/tools/compat5b.mlp b/tools/compat5b.mlp
new file mode 100644
index 000000000..0aa13dd64
--- /dev/null
+++ b/tools/compat5b.mlp
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
+ - EXTEND ... becomes EXTEND Gram ...
+*)
+
+open Camlp4.PreCast
+
+let rec my_token_filter = parser
+ | [< '(KEYWORD "EXTEND",_ as t); s >] ->
+ [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >]
+ | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
+ | [< >] -> [< >]
+
+let _ =
+ Token.Filter.define_filter (Gram.get_filter())
+ (fun prev strm -> prev (my_token_filter strm))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:16:49 +0000