aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/13842-proux01-remove-decimal.sh1
-rw-r--r--doc/changelog/03-notations/13842-remove-decimal.rst3
-rw-r--r--doc/sphinx/changes.rst4
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst6
-rw-r--r--interp/notation.ml40
-rw-r--r--interp/notation.mli3
-rw-r--r--plugins/syntax/number.ml24
-rw-r--r--tactics/hints.ml170
8 files changed, 105 insertions, 146 deletions
diff --git a/dev/ci/user-overlays/13842-proux01-remove-decimal.sh b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh
new file mode 100644
index 0000000000..5ede8221ce
--- /dev/null
+++ b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh
@@ -0,0 +1 @@
+overlay hott https://github.com/proux01/HoTT coq-13842 13842
diff --git a/doc/changelog/03-notations/13842-remove-decimal.rst b/doc/changelog/03-notations/13842-remove-decimal.rst
new file mode 100644
index 0000000000..4bc26ef6a8
--- /dev/null
+++ b/doc/changelog/03-notations/13842-remove-decimal.rst
@@ -0,0 +1,3 @@
+- **Removed:**
+ Remove decimal-only number notations which were deprecated in 8.12.
+ (`#13842 <https://github.com/coq/coq/pull/13842>`_, by Pierre Roux).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index ea099eb52e..8fa1b97851 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -82,13 +82,13 @@ Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack,
Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia
and Théo Zimmermann.
-The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric
+The 51 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric
Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed,
Cyril Cohen, Julien Coolen, Matthew Dempsky, Maxime Dénès, Andres Erbsen,
Jim Fehrle, Emilio Jesús Gallego Arias, Paolo G. Giarrusso, Attila Gáspár, Gaëtan Gilbert,
Jason Gross, Benjamin Grégoire, Hugo Herbelin, Wolf Honore, Jasper Hugunin, Ignat Insarov,
Ralf Jung, Fabian Kunze, Vincent Laporte, Olivier Laurent, Larry D. Lee Jr,
-Thomas Letan, Yishuai Li, Xia Li-yao, James Lottes, Jean-Christophe Léchenet,
+Thomas Letan, Yishuai Li, James Lottes, Jean-Christophe Léchenet,
Kenji Maillard, Erik Martin-Dorel, Yusuke Matsushita, Guillaume Melquiond,
Carl Patenaude-Poulin, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux,
Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Matthieu Sozeau,
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 03571ad680..557ef10555 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1726,12 +1726,6 @@ Number notations
* :n:`@qualid__type -> Number.number`
* :n:`@qualid__type -> option Number.number`
- .. deprecated:: 8.12
- Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and
- :g:`Decimal.decimal` are replaced respectively by number
- notations on :g:`Number.uint`, :g:`Number.int` and
- :g:`Number.number`.
-
When parsing, the application of the parsing function
:n:`@qualid__parse` to the number will be fully reduced, and universes
of the resulting term will be refreshed.
diff --git a/interp/notation.ml b/interp/notation.ml
index ed605c994d..4010c3487e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -557,9 +557,6 @@ type target_kind =
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
| Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *)
| Number of number_ty (* Coq.Init.Number.number + uint + int *)
- | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
- | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
- | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
type string_target_kind =
| ListByte
@@ -872,30 +869,16 @@ let mkDecHex ind c n = match c with
| CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Decimal *)
| CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hexadecimal *)
-exception NonDecimal
-
-let decimal_coqnumber_of_rawnum inds n =
- if NumTok.Signed.classify n <> CDec then raise NonDecimal;
- coqnumber_of_rawnum inds CDec n
-
let coqnumber_of_rawnum inds n =
let c = NumTok.Signed.classify n in
let n = coqnumber_of_rawnum inds c n in
mkDecHex inds.number c n
-let decimal_coquint_of_rawnum inds n =
- if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal;
- coquint_of_rawnum inds CDec (Some n)
-
let coquint_of_rawnum inds n =
let c = NumTok.UnsignedNat.classify n in
let n = coquint_of_rawnum inds c (Some n) in
mkDecHex inds.uint c n
-let decimal_coqint_of_rawnum inds n =
- if NumTok.SignedNat.classify n <> CDec then raise NonDecimal;
- coqint_of_rawnum inds CDec n
-
let coqint_of_rawnum inds n =
let c = NumTok.SignedNat.classify n in
let n = coqint_of_rawnum inds c n in
@@ -950,23 +933,14 @@ let destDecHex c = match Constr.kind c with
| _ -> raise NotAValidPrimToken)
| _ -> raise NotAValidPrimToken
-let decimal_rawnum_of_coqnumber c =
- rawnum_of_coqnumber CDec c
-
let rawnum_of_coqnumber c =
let cl, c = destDecHex c in
rawnum_of_coqnumber cl c
-let decimal_rawnum_of_coquint c =
- rawnum_of_coquint CDec c
-
let rawnum_of_coquint c =
let cl, c = destDecHex c in
rawnum_of_coquint cl c
-let decimal_rawnum_of_coqint c =
- rawnum_of_coqint CDec c
-
let rawnum_of_coqint c =
let cl, c = destDecHex c in
rawnum_of_coqint cl c
@@ -1084,22 +1058,13 @@ let interp o ?loc n =
coqint_of_rawnum int_ty n
| UInt int_ty, Some (SPlus, n) ->
coquint_of_rawnum int_ty n
- | DecimalInt int_ty, Some n ->
- (try decimal_coqint_of_rawnum int_ty n
- with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
- | DecimalUInt int_ty, Some (SPlus, n) ->
- (try decimal_coquint_of_rawnum int_ty n
- with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
| Z z_pos_ty, Some n ->
z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n)
| Int63 pos_neg_int63_ty, Some n ->
interp_int63 ?loc pos_neg_int63_ty.pos_neg_int63_ty (NumTok.SignedNat.to_bigint n)
- | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63 _), _ ->
+ | (Int _ | UInt _ | Z _ | Int63 _), _ ->
no_such_prim_token "number" ?loc o.ty_name
| Number number_ty, _ -> coqnumber_of_rawnum number_ty n
- | Decimal number_ty, _ ->
- (try decimal_coqnumber_of_rawnum number_ty n
- with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
in
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -1124,9 +1089,6 @@ let uninterp o n =
| (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c)
| (Int63 _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_coqpos_neg_int63 c)
| (Number _, c) -> rawnum_of_coqnumber c
- | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c)
- | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c)
- | (Decimal _, c) -> decimal_rawnum_of_coqnumber c
end o n
end
diff --git a/interp/notation.mli b/interp/notation.mli
index 77f245ae77..195f2a4416 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -146,9 +146,6 @@ type target_kind =
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
| Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *)
| Number of number_ty (* Coq.Init.Number.number + uint + int *)
- | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
- | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
- | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
type string_target_kind =
| ListByte
diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml
index 80c11dc0d4..551e2bac5d 100644
--- a/plugins/syntax/number.ml
+++ b/plugins/syntax/number.ml
@@ -131,13 +131,6 @@ let type_error_of g ty =
str " to Number.int or (option Number.int)." ++ fnl () ++
str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).")
-let warn_deprecated_decimal =
- CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated"
- (fun () ->
- strbrk "Deprecated Number Notation for Decimal.uint, \
- Decimal.int or Decimal.decimal. Use Number.uint, \
- Number.int or Number.number respectively.")
-
let error_params ind =
CErrors.user_err
(str "Wrong number of parameters for inductive" ++ spc ()
@@ -456,12 +449,6 @@ let vernac_number_notation local ty f g opts scope =
| Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option
| Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct
| Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option
- | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct
- | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option
- | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct
- | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option
- | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct
- | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct
@@ -484,12 +471,6 @@ let vernac_number_notation local ty f g opts scope =
| Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option
| Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct
| Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option
- | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct
- | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option
- | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct
- | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option
- | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct
- | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct
@@ -500,11 +481,6 @@ let vernac_number_notation local ty f g opts scope =
| Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty (opt cint63)) -> Int63 pos_neg_int63_ty, Option
| _ -> type_error_of g ty
in
- (match to_kind, of_kind with
- | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _
- | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) ->
- warn_deprecated_decimal ()
- | _ -> ());
let to_post, pt_required, pt_refs = match tyc_params with
| TargetPrim path -> [||], path, [Coqlib.lib_ref "num.int63.wrap_int"]
| TargetInd (tyc, params) ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 058602acfd..5e9c3baeb1 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1019,18 +1019,6 @@ let remove_hint dbname grs =
let db' = Hint_db.remove_list env grs db in
searchtable_add (dbname, db')
-type hint_action =
- | CreateDB of bool * TransparentState.t
- | AddTransparency of {
- superglobal : bool;
- grefs : evaluable_global_reference hints_transparency_target;
- state : bool;
- }
- | AddHints of { superglobal : bool; hints : hint_entry list }
- | RemoveHints of { superglobal : bool; hints : GlobRef.t list }
- | AddCut of { superglobal : bool; paths : hints_path }
- | AddMode of { superglobal : bool; gref : GlobRef.t; mode : hint_mode array }
-
let add_cut dbname path =
let db = get_db dbname in
let db' = Hint_db.add_cut path db in
@@ -1041,30 +1029,72 @@ let add_mode dbname l m =
let db' = Hint_db.add_mode l m db in
searchtable_add (dbname, db')
+type db_obj = {
+ db_local : bool;
+ db_name : string;
+ db_use_dn : bool;
+ db_ts : TransparentState.t;
+}
+
+let cache_db (_, {db_name=name; db_use_dn=b; db_ts=ts}) =
+ searchtable_add (name, Hint_db.empty ~name ts b)
+
+let load_db _ x = cache_db x
+
+let classify_db db = if db.db_local then Dispose else Substitute db
+
+let inDB : db_obj -> obj =
+ declare_object {(default_object "AUTOHINT_DB") with
+ cache_function = cache_db;
+ load_function = load_db;
+ subst_function = (fun (_,x) -> x);
+ classify_function = classify_db; }
+
+let create_hint_db l n ts b =
+ let hint = {db_local=l; db_name=n; db_use_dn=b; db_ts=ts} in
+ Lib.add_anonymous_leaf (inDB hint)
+
+type hint_action =
+ | AddTransparency of {
+ grefs : evaluable_global_reference hints_transparency_target;
+ state : bool;
+ }
+ | AddHints of hint_entry list
+ | RemoveHints of GlobRef.t list
+ | AddCut of hints_path
+ | AddMode of { gref : GlobRef.t; mode : hint_mode array }
+
+type hint_locality = Local | Export | SuperGlobal
+
type hint_obj = {
- hint_local : bool;
+ hint_local : hint_locality;
hint_name : string;
hint_action : hint_action;
}
+let superglobal h = match h.hint_local with
+ | SuperGlobal -> true
+ | Local | Export -> false
+
let load_autohint _ (kn, h) =
let name = h.hint_name in
+ let superglobal = superglobal h in
match h.hint_action with
- | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b)
- | AddTransparency { superglobal; grefs; state } ->
+ | AddTransparency { grefs; state } ->
if superglobal then add_transparency name grefs state
- | AddHints { superglobal; hints } ->
+ | AddHints hints ->
if superglobal then add_hint name hints
- | RemoveHints { superglobal; hints } ->
+ | RemoveHints hints ->
if superglobal then remove_hint name hints
- | AddCut { superglobal; paths } ->
+ | AddCut paths ->
if superglobal then add_cut name paths
- | AddMode { superglobal; gref; mode } ->
+ | AddMode { gref; mode } ->
if superglobal then add_mode name gref mode
let open_autohint i (kn, h) =
+ let superglobal = superglobal h in
if Int.equal i 1 then match h.hint_action with
- | AddHints { superglobal; hints } ->
+ | AddHints hints ->
let () =
if not superglobal then
(* Import-bound hints must be declared when not imported yet *)
@@ -1073,15 +1103,14 @@ let open_autohint i (kn, h) =
in
let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in
List.iter add hints
- | AddCut { superglobal; paths } ->
+ | AddCut paths ->
if not superglobal then add_cut h.hint_name paths
- | AddTransparency { superglobal; grefs; state } ->
+ | AddTransparency { grefs; state } ->
if not superglobal then add_transparency h.hint_name grefs state
- | RemoveHints { superglobal; hints } ->
+ | RemoveHints hints ->
if not superglobal then remove_hint h.hint_name hints
- | AddMode { superglobal; gref; mode } ->
+ | AddMode { gref; mode } ->
if not superglobal then add_mode h.hint_name gref mode
- | CreateDB _ -> ()
let cache_autohint (kn, obj) =
load_autohint 1 (kn, obj); open_autohint 1 (kn, obj)
@@ -1137,8 +1166,7 @@ let subst_autohint (subst, obj) =
if k' == k && data' == data then hint else (k',data')
in
let action = match obj.hint_action with
- | CreateDB _ -> obj.hint_action
- | AddTransparency { superglobal; grefs = target; state = b } ->
+ | AddTransparency { grefs = target; state = b } ->
let target' =
match target with
| HintsVariables -> target
@@ -1148,26 +1176,28 @@ let subst_autohint (subst, obj) =
if grs == grs' then target
else HintsReferences grs'
in
- if target' == target then obj.hint_action else AddTransparency { superglobal; grefs = target'; state = b }
- | AddHints { superglobal; hints } ->
+ if target' == target then obj.hint_action else AddTransparency { grefs = target'; state = b }
+ | AddHints hints ->
let hints' = List.Smart.map subst_hint hints in
- if hints' == hints then obj.hint_action else AddHints { superglobal; hints = hints' }
- | RemoveHints { superglobal; hints = grs } ->
+ if hints' == hints then obj.hint_action else AddHints hints'
+ | RemoveHints grs ->
let grs' = List.Smart.map (subst_global_reference subst) grs in
- if grs == grs' then obj.hint_action else RemoveHints { superglobal; hints = grs' }
- | AddCut { superglobal; paths = path } ->
+ if grs == grs' then obj.hint_action else RemoveHints grs'
+ | AddCut path ->
let path' = subst_hints_path subst path in
- if path' == path then obj.hint_action else AddCut { superglobal; paths = path' }
- | AddMode { superglobal; gref = l; mode = m } ->
+ if path' == path then obj.hint_action else AddCut path'
+ | AddMode { gref = l; mode = m } ->
let l' = subst_global_reference subst l in
- if l' == l then obj.hint_action else AddMode { superglobal; gref = l'; mode = m }
+ if l' == l then obj.hint_action else AddMode { gref = l'; mode = m }
in
if action == obj.hint_action then obj else { obj with hint_action = action }
let classify_autohint obj =
match obj.hint_action with
- | AddHints { hints = [] } -> Dispose
- | _ -> if obj.hint_local then Dispose else Substitute obj
+ | AddHints [] -> Dispose
+ | _ -> match obj.hint_local with
+ | Local -> Dispose
+ | Export | SuperGlobal -> Substitute obj
let inAutoHint : hint_obj -> obj =
declare_object {(default_object "AUTOHINT") with
@@ -1177,16 +1207,12 @@ let inAutoHint : hint_obj -> obj =
subst_function = subst_autohint;
classify_function = classify_autohint; }
-let make_hint ?(local = false) name action = {
+let make_hint ~local name action = {
hint_local = local;
hint_name = name;
hint_action = action;
}
-let create_hint_db l n st b =
- let hint = make_hint ~local:l n (CreateDB (b, st)) in
- Lib.add_anonymous_leaf (inAutoHint hint)
-
let warn_deprecated_hint_without_locality =
CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated"
(fun () -> strbrk "The default value for hint locality is currently \
@@ -1210,16 +1236,16 @@ let check_hint_locality = let open Goptions in function
| OptLocal -> ()
let interp_locality = function
-| Goptions.OptDefault | Goptions.OptGlobal -> false, true
-| Goptions.OptExport -> false, false
-| Goptions.OptLocal -> true, false
+| Goptions.OptDefault | Goptions.OptGlobal -> SuperGlobal
+| Goptions.OptExport -> Export
+| Goptions.OptLocal -> Local
let remove_hints ~locality dbnames grs =
- let local, superglobal = interp_locality locality in
+ let local = interp_locality locality in
let dbnames = if List.is_empty dbnames then ["core"] else dbnames in
List.iter
(fun dbname ->
- let hint = make_hint ~local dbname (RemoveHints { superglobal; hints = grs }) in
+ let hint = make_hint ~local dbname (RemoveHints grs) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
@@ -1227,7 +1253,7 @@ let remove_hints ~locality dbnames grs =
(* The "Hint" vernacular command *)
(**************************************************************************)
-let add_resolves env sigma clist ~local ~superglobal dbnames =
+let add_resolves env sigma clist ~local dbnames =
List.iter
(fun dbname ->
let r =
@@ -1254,56 +1280,56 @@ let add_resolves env sigma clist ~local ~superglobal dbnames =
| _ -> ()
in
let () = if not !Flags.quiet then List.iter check r in
- let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in
+ let hint = make_hint ~local dbname (AddHints r) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_unfolds l ~local ~superglobal dbnames =
+let add_unfolds l ~local dbnames =
List.iter
(fun dbname ->
- let hint = make_hint ~local dbname (AddHints { superglobal; hints = List.map make_unfold l }) in
+ let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_cuts l ~local ~superglobal dbnames =
+let add_cuts l ~local dbnames =
List.iter
(fun dbname ->
- let hint = make_hint ~local dbname (AddCut { superglobal; paths = l }) in
+ let hint = make_hint ~local dbname (AddCut l) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_mode l m ~local ~superglobal dbnames =
+let add_mode l m ~local dbnames =
List.iter
(fun dbname ->
let m' = make_mode l m in
- let hint = make_hint ~local dbname (AddMode { superglobal; gref = l; mode = m' }) in
+ let hint = make_hint ~local dbname (AddMode { gref = l; mode = m' }) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_transparency l b ~local ~superglobal dbnames =
+let add_transparency l b ~local dbnames =
List.iter
(fun dbname ->
- let hint = make_hint ~local dbname (AddTransparency { superglobal; grefs = l; state = b }) in
+ let hint = make_hint ~local dbname (AddTransparency { grefs = l; state = b }) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_extern info tacast ~local ~superglobal dbname =
+let add_extern info tacast ~local dbname =
let pat = match info.hint_pattern with
| None -> None
| Some (_, pat) -> Some pat
in
let hint = make_hint ~local dbname
- (AddHints { superglobal; hints = [make_extern (Option.get info.hint_priority) pat tacast] }) in
+ (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
Lib.add_anonymous_leaf (inAutoHint hint)
-let add_externs info tacast ~local ~superglobal dbnames =
- List.iter (add_extern info tacast ~local ~superglobal) dbnames
+let add_externs info tacast ~local dbnames =
+ List.iter (add_extern info tacast ~local) dbnames
-let add_trivials env sigma l ~local ~superglobal dbnames =
+let add_trivials env sigma l ~local dbnames =
List.iter
(fun dbname ->
let l = List.map (fun (name, c) -> make_trivial env sigma ~name c) l in
- let hint = make_hint ~local dbname (AddHints { superglobal; hints = l }) in
+ let hint = make_hint ~local dbname (AddHints l) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
@@ -1360,22 +1386,22 @@ let prepare_hint check env init (sigma,c) =
(c', diff)
let add_hints ~locality dbnames h =
- let local, superglobal = interp_locality locality in
+ let local = interp_locality locality in
if String.List.mem "nocore" dbnames then
user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
assert (not (List.is_empty dbnames));
let env = Global.env() in
let sigma = Evd.from_env env in
match h with
- | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames
- | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames
- | HintsCutEntry lhints -> add_cuts lhints ~local ~superglobal dbnames
- | HintsModeEntry (l,m) -> add_mode l m ~local ~superglobal dbnames
- | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames
+ | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local dbnames
+ | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local dbnames
+ | HintsCutEntry lhints -> add_cuts lhints ~local dbnames
+ | HintsModeEntry (l,m) -> add_mode l m ~local dbnames
+ | HintsUnfoldEntry lhints -> add_unfolds lhints ~local dbnames
| HintsTransparencyEntry (lhints, b) ->
- add_transparency lhints b ~local ~superglobal dbnames
+ add_transparency lhints b ~local dbnames
| HintsExternEntry (info, tacexp) ->
- add_externs info tacexp ~local ~superglobal dbnames
+ add_externs info tacexp ~local dbnames
let hint_globref gr = IsGlobRef gr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:15:28 +0000