aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml42
-rw-r--r--grammar/gramCompat.ml486
-rw-r--r--grammar/grammar.mllib10
-rw-r--r--grammar/q_constr.ml410
-rw-r--r--grammar/q_util.ml46
-rw-r--r--grammar/q_util.mli2
-rw-r--r--grammar/tacextend.ml46
-rw-r--r--grammar/vernacextend.ml46
8 files changed, 100 insertions, 28 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 9be6c6bc4..8e06adce9 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -9,7 +9,7 @@
(*i camlp4deps: "tools/compat5b.cmo" i*)
open Q_util
-open Compat
+open GramCompat
let loc = CompatLoc.ghost
let default_loc = <:expr< Loc.ghost >>
diff --git a/grammar/gramCompat.ml4 b/grammar/gramCompat.ml4
new file mode 100644
index 000000000..6246da7bb
--- /dev/null
+++ b/grammar/gramCompat.ml4
@@ -0,0 +1,86 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Compatibility file depending on ocaml/camlp4 version *)
+
+(** Misc module emulation *)
+
+IFDEF CAMLP5 THEN
+
+module CompatLoc = struct
+ include Ploc
+ let ghost = dummy
+ let merge = encl
+end
+
+ELSE
+
+module CompatLoc = Camlp4.PreCast.Loc
+
+END
+
+IFDEF CAMLP5 THEN
+
+module PcamlSig = struct end
+
+ELSE
+
+module PcamlSig = Camlp4.Sig
+module Ast = Camlp4.PreCast.Ast
+module Pcaml = Camlp4.PreCast.Syntax
+module MLast = Ast
+
+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, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
+ELSE
+ Ast.stSem_of_list l
+END
+
+(** Quotation difference for match clauses *)
+
+let default_patt loc =
+ (<: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, vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *)
+
+ELSE
+
+let make_fun loc cl =
+ let mk_when = function
+ | Some w -> w
+ | None -> Ast.ExNil loc
+ in
+ let mk_clause (patt,optwhen,expr) =
+ (* correspond to <:match_case< ... when ... -> ... >> *)
+ Ast.McArr (loc, patt, mk_when optwhen, expr) in
+ let init = mk_clause (default_patt loc) in
+ let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in
+ let l = List.fold_right add_clause cl init in
+ Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *)
+
+END
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 9b24c9797..6c3ce7f03 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,12 +1,4 @@
-Coq_config
-
-Store
-Exninfo
-Loc
-
-Tok
-Compat
-
+GramCompat
Q_util
Argextend
Tacextend
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4
index 40db81949..af90f5f2a 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.ml4
@@ -9,7 +9,7 @@
(*i camlp4deps: "tools/compat5b.cmo" i*)
open Q_util
-open Compat
+open GramCompat
open Pcaml
open PcamlSig (* necessary for camlp4 *)
@@ -27,11 +27,6 @@ EXTEND
[ [ "PATTERN"; "["; c = constr; "]" ->
<:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ]
;
- sort:
- [ [ "Set" -> Misctypes.GSet
- | "Prop" -> Misctypes.GProp
- | "Type" -> Misctypes.GType [] ] ]
- ;
ident:
[ [ s = string -> <:expr< Names.Id.of_string $str:s$ >> ] ]
;
@@ -68,8 +63,7 @@ EXTEND
let args = mlexpr_of_list (fun x -> x) args in
<:expr< Glob_term.GApp ($dloc$,$f$,$args$) >> ]
| "0"
- [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >>
- | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >>
+ [ id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >>
| "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False),Misctypes.IntroAnonymous,None) >>
| "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >>
| "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index a9a339241..2d5c40894 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -8,7 +8,7 @@
(* This file defines standard combinators to build ml expressions *)
-open Compat
+open GramCompat
type argument_type =
| ListArgType of argument_type
@@ -87,7 +87,7 @@ let coincide s pat off =
while !break && !i < len do
let c = Char.code s.[off + !i] in
let d = Char.code pat.[!i] in
- break := Int.equal c d;
+ break := c = d;
incr i
done;
!break
@@ -110,7 +110,7 @@ let rec parse_user_entry s sep =
else if l > 4 && coincide s "_opt" (l-4) then
let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
Uopt entry
- else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
+ else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
let n = Char.code s.[6] - 48 in
Uentryl ("tactic", n)
else
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 9b6f11827..a5e36e47b 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Compat (* necessary for camlp4 *)
+open GramCompat (* necessary for camlp4 *)
type argument_type =
| ListArgType of argument_type
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 4c4ecaf73..8593bad5d 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -12,7 +12,7 @@
open Q_util
open Argextend
-open Compat
+open GramCompat
let dloc = <:expr< Loc.ghost >>
@@ -47,7 +47,7 @@ let make_clause (pt,_,e) =
make_let false e pt)
let make_fun_clauses loc s l =
- let map c = Compat.make_fun loc [make_clause c] in
+ let map c = GramCompat.make_fun loc [make_clause c] in
mlexpr_of_list map l
let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >>
@@ -102,7 +102,7 @@ let declare_tactic loc s c cl = match cl with
whole-prof tactics like [shelve_unifiable]. *)
<:expr< fun _ $lid:"ist"$ -> $tac$ >>
| _ ->
- let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
+ let f = GramCompat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
<:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
in
(** Arguments are not passed directly to the ML tactic in the TacML node,
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 904662ea1..1611de39c 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -13,7 +13,7 @@
open Q_util
open Argextend
open Tacextend
-open Compat
+open GramCompat
type rule = {
r_head : string option;
@@ -93,13 +93,13 @@ let make_fun_clauses loc s l =
| None -> false
| Some () -> true
in
- let cl = Compat.make_fun loc [make_clause c] in
+ let cl = GramCompat.make_fun loc [make_clause c] in
<:expr< ($mlexpr_of_bool depr$, $cl$)>>
in
mlexpr_of_list map l
let make_fun_classifiers loc s c l =
- let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
+ let cl = List.map (fun x -> GramCompat.make_fun loc [make_clause_classifier c s x]) l in
mlexpr_of_list (fun x -> x) cl
let make_prod_item = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 14:38:12 +0000