aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_ast.mli1
-rw-r--r--coqpp/coqpp_lex.mll1
-rw-r--r--coqpp/coqpp_main.ml11
-rw-r--r--coqpp/coqpp_parse.mly11
-rw-r--r--default.nix2
-rw-r--r--doc/sphinx/addendum/extended-pattern-matching.rst11
-rw-r--r--doc/sphinx/addendum/implicit-coercions.rst6
-rw-r--r--grammar/tacextend.mlp2
-rw-r--r--pretyping/classops.ml28
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/coercion.ml9
-rw-r--r--tools/coq_dune.ml30
12 files changed, 92 insertions, 22 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 39b4d2ab34..181c43615b 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -81,6 +81,7 @@ type grammar_ext = {
type tactic_ext = {
tacext_name : string;
tacext_level : int option;
+ tacext_deprecated : code option;
tacext_rules : tactic_rule list;
}
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index 6c6562c204..bfa4e2b57b 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -95,6 +95,7 @@ rule extend = parse
| "END" { END }
| "DECLARE" { DECLARE }
| "PLUGIN" { PLUGIN }
+| "DEPRECATED" { DEPRECATED }
(** Camlp5 specific keywords *)
| "GLOBAL" { GLOBAL }
| "FIRST" { FIRST }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 1648167a27..a8ed95f5ba 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -316,10 +316,17 @@ let print_rules fmt rules =
fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules
let print_ast fmt ext =
+ let deprecation fmt =
+ function
+ | None -> ()
+ | Some { code } -> fprintf fmt "~deprecation:(%s) " code
+ in
let pr fmt () =
let level = match ext.tacext_level with None -> 0 | Some i -> i in
- fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a"
- plugin_name ext.tacext_name level print_rules ext.tacext_rules
+ fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a%a"
+ plugin_name ext.tacext_name level
+ deprecation ext.tacext_deprecated
+ print_rules ext.tacext_rules
in
let () = fprintf fmt "let () = @[%a@]\n" pr () in
()
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index baafd633c4..bf435fd247 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -62,7 +62,7 @@ let parse_user_entry s sep =
%token <string> IDENT QUALID
%token <string> STRING
%token <int> INT
-%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN
+%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED
%token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL
%token LPAREN RPAREN COLON SEMICOLON
%token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
@@ -108,8 +108,13 @@ vernac_extend:
;
tactic_extend:
-| TACTIC EXTEND IDENT tactic_level tactic_rules END
- { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } }
+| TACTIC EXTEND IDENT tactic_deprecated tactic_level tactic_rules END
+ { TacticExt { tacext_name = $3; tacext_deprecated = $4; tacext_level = $5; tacext_rules = $6 } }
+;
+
+tactic_deprecated:
+| { None }
+| DEPRECATED CODE { Some $2 }
;
tactic_level:
diff --git a/default.nix b/default.nix
index 35da15eebd..80dca47f69 100644
--- a/default.nix
+++ b/default.nix
@@ -76,7 +76,7 @@ stdenv.mkDerivation rec {
)
++ optionals shell (
[ jq curl git gnupg ] # Dependencies of the merging script
- ++ (with ocamlPackages; [ merlin ocp-indent ocp-index ]) # Dev tools
+ ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ]) # Dev tools
);
src =
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index f7fd4b9146..e507a224c6 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -407,12 +407,11 @@ length, by writing
.. coqtop:: in
- Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
- listn (n + m) :=
- match l in listn n, l' return listn (n + m) with
- | niln, x => x
- | consn n' a y, x => consn (n' + m) a (concat n' y m x)
- end.
+ Check (fun n (a b: listn n) =>
+ match a, b with
+ | niln, b0 => tt
+ | consn n' a y, bS => tt
+ end).
we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`.
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index c0c4539564..23cbd76eda 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -325,6 +325,12 @@ Coercions and Modules
This option makes it possible to recover the behavior of the versions of
|Coq| prior to 8.3.
+.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it.
+
+ This warning is emitted when typechecking relies on a coercion
+ contained in a module that has not been explicitely imported. It helps
+ migrating code and stop relying on the option above.
+
Examples
--------
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 07239e7af0..5943600b7c 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+(** WARNING: this file is deprecated; consider modifying coqpp instead. *)
+
(** Implementation of the TACTIC EXTEND macro. *)
open Q_util
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 542fb5456c..52e02c87fd 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -118,6 +118,9 @@ let class_tab =
let coercion_tab =
ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
+let coercions_in_scope =
+ ref Refset_env.empty
+
module ClPairOrd =
struct
type t = cl_index * cl_index
@@ -131,12 +134,13 @@ module ClPairMap = Map.Make(ClPairOrd)
let inheritance_graph =
ref (ClPairMap.empty : inheritance_path ClPairMap.t)
-let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph)
+let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope)
-let unfreeze (fcl,fco,fig) =
+let unfreeze (fcl,fco,fig,in_scope) =
class_tab:=fcl;
coercion_tab:=fco;
- inheritance_graph:=fig
+ inheritance_graph:=fig;
+ coercions_in_scope:=in_scope
(* ajout de nouveaux "objets" *)
@@ -445,9 +449,16 @@ let load_coercion _ o =
if !automatically_import_coercions then
cache_coercion (Global.env ()) Evd.empty o
+let set_coercion_in_scope (_, c) =
+ let r = c.coercion_type in
+ coercions_in_scope := Refset_env.add r !coercions_in_scope
+
let open_coercion i o =
- if Int.equal i 1 && not !automatically_import_coercions then
- cache_coercion (Global.env ()) Evd.empty o
+ if Int.equal i 1 then begin
+ set_coercion_in_scope o;
+ if not !automatically_import_coercions then
+ cache_coercion (Global.env ()) Evd.empty o
+ end
let subst_coercion (subst, c) =
let coe = subst_coe_typ subst c.coercion_type in
@@ -492,7 +503,9 @@ let inCoercion : coercion -> obj =
open_function = open_coercion;
load_function = load_coercion;
cache_function = (fun objn ->
- let env = Global.env () in cache_coercion env Evd.empty objn
+ let env = Global.env () in
+ set_coercion_in_scope objn;
+ cache_coercion env Evd.empty objn
);
subst_function = subst_coercion;
classify_function = classify_coercion;
@@ -553,3 +566,6 @@ let hide_coercion coe =
let coe_info = coercion_info coe in
Some coe_info.coe_param
else None
+
+let is_coercion_in_scope r =
+ Refset_env.mem r !coercions_in_scope
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index af00c0a8dc..dc193c4e74 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -113,3 +113,5 @@ val coercions : unit -> coe_info_typ list
(** [hide_coercion] returns the number of params to skip if the coercion must
be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
val hide_coercion : coe_typ -> int option
+
+val is_coercion_in_scope : GlobRef.t -> bool
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5e3821edf1..e15c00f7dc 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -363,12 +363,20 @@ let saturate_evd env evd =
Typeclasses.resolve_typeclasses
~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
+let warn_coercion_not_in_scope =
+ CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated"
+ Pp.(fun r -> str "Coercion used but not in scope: " ++
+ Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use "
+ ++ str "this coercion, please Import the module that contains it.")
+
(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
let apply_coercion env sigma p hj typ_cl =
try
let j,t,evd =
List.fold_left
(fun (ja,typ_cl,sigma) i ->
+ if not (is_coercion_in_scope i.coe_value) then
+ warn_coercion_not_in_scope i.coe_value;
let isid = i.coe_is_identity in
let isproj = i.coe_is_projection in
let sigma, c = new_global sigma i.coe_value in
@@ -386,7 +394,6 @@ let apply_coercion env sigma p hj typ_cl =
(hj,typ_cl,sigma) p
in evd, j
with NoCoercion as e -> raise e
- | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.")
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core env evd j =
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index c89c78c8ec..ab60920fbc 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -80,6 +80,7 @@ module Aux = struct
module DirMap = Map.Make(DirOrd)
(* Functions available in newer OCaml versions *)
+ (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *)
module Legacy = struct
(* Slower version of DirMap.update, waiting for OCaml 4.06.0 *)
@@ -103,6 +104,29 @@ module Aux = struct
end
done;
sub s 0 !j :: !r
+
+ (* Available in OCaml >= 4.04 *)
+ let is_dir_sep = match Sys.os_type with
+ | "Win32" -> fun s i -> s.[i] = '\\'
+ | _ -> fun s i -> s.[i] = '/'
+
+ let extension_len name =
+ let rec check i0 i =
+ if i < 0 || is_dir_sep name i then 0
+ else if name.[i] = '.' then check i0 (i - 1)
+ else String.length name - i0
+ in
+ let rec search_dot i =
+ if i < 0 || is_dir_sep name i then 0
+ else if name.[i] = '.' then check i (i - 1)
+ else search_dot (i - 1)
+ in
+ search_dot (String.length name - 1)
+
+ let remove_extension name =
+ let l = extension_len name in
+ if l = 0 then name else String.sub name 0 (String.length name - l)
+
end
let add_map_list key elem map =
@@ -181,18 +205,18 @@ let pp_vo_dep dir fmt vo =
(* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *)
let deps = List.map (fun s -> sdir ^ s) (edep @ vo.deps) in
(* The source file is also corrected as we will call coqtop from the top dir *)
- let source = String.concat "/" dir ^ "/" ^ Filename.(remove_extension vo.target) ^ ".v" in
+ let source = String.concat "/" dir ^ "/" ^ Legacy.(remove_extension vo.target) ^ ".v" in
(* The final build rule *)
let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in
pp_rule fmt [vo.target] deps action
let pp_ml4_dep _dir fmt ml =
- let target = Filename.(remove_extension ml) ^ ".ml" in
+ let target = Legacy.(remove_extension ml) ^ ".ml" in
let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in
pp_rule fmt [target] [ml] ml4_rule
let pp_mlg_dep _dir fmt ml =
- let target = Filename.(remove_extension ml) ^ ".ml" in
+ let target = Legacy.(remove_extension ml) ^ ".ml" in
let ml4_rule = "(run coqpp %{pp-file})" in
pp_rule fmt [target] [ml] ml4_rule
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 21:18:39 +0000