aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.ml33
-rw-r--r--engine/evarutil.mli9
-rw-r--r--engine/evd.ml56
-rw-r--r--engine/evd.mli14
-rw-r--r--engine/ftactic.ml7
-rw-r--r--engine/ftactic.mli3
-rw-r--r--engine/nameops.ml85
-rw-r--r--engine/nameops.mli34
-rw-r--r--engine/proofview.ml52
-rw-r--r--engine/proofview.mli32
-rw-r--r--engine/termops.ml20
-rw-r--r--engine/termops.mli24
-rw-r--r--engine/uState.ml4
-rw-r--r--engine/uState.mli3
-rw-r--r--engine/univGen.ml42
-rw-r--r--engine/univGen.mli27
-rw-r--r--engine/univMinim.ml2
17 files changed, 194 insertions, 253 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 96beb72a56..0a5bba39b9 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -26,24 +26,7 @@ let safe_evar_value sigma ev =
try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev)
with NotInstantiatedEvar | Not_found -> None
-(** Combinators *)
-
-let evd_comb0 f evdref =
- let (evd',x) = f !evdref in
- evdref := evd';
- x
-
-let evd_comb1 f evdref x =
- let (evd',y) = f !evdref x in
- evdref := evd';
- y
-
-let evd_comb2 f evdref x y =
- let (evd',z) = f !evdref x y in
- evdref := evd';
- z
-
-let new_global evd x =
+let new_global evd x =
let (evd, c) = Evd.fresh_global (Global.env()) evd x in
(evd, c)
@@ -673,26 +656,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids =
(* spiwack: a few functions to gather evars on which goals depend. *)
let queue_set q is_dependent set =
Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
-let queue_term q is_dependent c =
- queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c))
+let queue_term evm q is_dependent c =
+ queue_set q is_dependent (evars_of_term evm c)
let process_dependent_evar q acc evm is_dependent e =
let evi = Evd.find evm e in
(* Queues evars appearing in the types of the goal (conclusion, then
hypotheses), they are all dependent. *)
- queue_term q true evi.evar_concl;
+ queue_term evm q true evi.evar_concl;
List.iter begin fun decl ->
let open NamedDecl in
- queue_term q true (NamedDecl.get_type decl);
+ queue_term evm q true (NamedDecl.get_type decl);
match decl with
| LocalAssum _ -> ()
- | LocalDef (_,b,_) -> queue_term q true b
+ | LocalDef (_,b,_) -> queue_term evm q true b
end (EConstr.named_context_of_val evi.evar_hyps);
match evi.evar_body with
| Evar_empty ->
if is_dependent then Evar.Map.add e None acc else acc
| Evar_defined b ->
- let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in
+ let subevars = evars_of_term evm b in
(* evars appearing in the definition of an evar [e] are marked
as dependent when [e] is dependent itself: if [e] is a
non-dependent goal, then, unless they are reach from another
@@ -812,7 +795,7 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi =
in
let accu = match evi.evar_body with
| Evar_empty -> Evar.Set.empty
- | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b)
+ | Evar_defined b -> evars_of_term sigma b
in
let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in
let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index bb0da44103..8eaff8bd13 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -274,15 +274,6 @@ val push_rel_context_to_named_context : ?hypnaming:naming_mode ->
val generalize_evar_over_rels : evar_map -> existential -> types * constr list
-(** Evar combinators *)
-
-val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-
val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located ->
Evar_kinds.t Loc.located
diff --git a/engine/evd.ml b/engine/evd.ml
index b89222cf8e..0f10a380d3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -823,33 +823,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
| Evar (evk2,_) -> fst (evar_source evk2 evd)
| _ -> None
-(** The following functions return the set of evars immediately
- contained in the object *)
-
-(* excluding defined evars *)
-
-let evars_of_term c =
- let rec evrec acc c =
- match kind c with
- | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
- | _ -> Constr.fold evrec acc c
- in
- evrec Evar.Set.empty c
-
-let evars_of_named_context nc =
- Context.Named.fold_outside
- (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr)))
- nc
- ~init:Evar.Set.empty
-
-let evars_of_filtered_evar_info evi =
- Evar.Set.union (evars_of_term evi.evar_concl)
- (Evar.Set.union
- (match evi.evar_body with
- | Evar_empty -> Evar.Set.empty
- | Evar_defined b -> evars_of_term b)
- (evars_of_named_context (evar_filtered_context evi)))
-
(**********************************************************)
(* Sort variables *)
@@ -869,8 +842,6 @@ let to_universe_context evd = UState.context evd.universes
let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
-let const_univ_entry = univ_entry
-
let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
let restrict_universe_context evd vars =
@@ -1406,3 +1377,30 @@ module MiniEConstr = struct
let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
end
+
+(** The following functions return the set of evars immediately
+ contained in the object *)
+
+(* excluding defined evars *)
+
+let evars_of_term evd c =
+ let rec evrec acc c =
+ match MiniEConstr.kind evd c with
+ | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+ | _ -> Constr.fold evrec acc c
+ in
+ evrec Evar.Set.empty c
+
+let evars_of_named_context evd nc =
+ Context.Named.fold_outside
+ (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term evd constr)))
+ nc
+ ~init:Evar.Set.empty
+
+let evars_of_filtered_evar_info evd evi =
+ Evar.Set.union (evars_of_term evd evi.evar_concl)
+ (Evar.Set.union
+ (match evi.evar_body with
+ | Evar_empty -> Evar.Set.empty
+ | Evar_defined b -> evars_of_term evd b)
+ (evars_of_named_context evd (evar_filtered_context evi)))
diff --git a/engine/evd.mli b/engine/evd.mli
index b0fcddb068..587a1de044 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -491,16 +491,15 @@ val extract_changed_conv_pbs : evar_map ->
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
-(** The following functions return the set of evars immediately
- contained in the object; need the term to be evar-normal otherwise
- defined evars are returned too. *)
+(** The following functions return the set of undefined evars
+ contained in the object. *)
-val evars_of_term : constr -> Evar.Set.t
+val evars_of_term : evar_map -> econstr -> Evar.Set.t
(** including evars in instances of evars *)
-val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t
+val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t
-val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
+val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t
(** Metas *)
val meta_list : evar_map -> (metavariable * clbinding) list
@@ -615,9 +614,6 @@ val to_universe_context : evar_map -> Univ.UContext.t
val univ_entry : poly:bool -> evar_map -> Entries.universes_entry
-val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry
val merge_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index ac0344148a..dab2e7d5ef 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -56,13 +56,6 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
-let nf_enter f =
- bind goals
- (fun gl ->
- gl >>= fun gl ->
- Proofview.Goal.normalize gl >>= fun nfgl ->
- Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"]
-
let enter f =
bind goals
(fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 3c4fa6f4e8..ed95d62bc6 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -41,9 +41,6 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
(** {5 Focussing} *)
-val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
-[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
-
(** Enter a goal. The resulting tactic is focussed. *)
val enter : (Proofview.Goal.t -> 'a t) -> 'a t
diff --git a/engine/nameops.ml b/engine/nameops.ml
index 2047772cfe..31914f9cfa 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -13,6 +13,51 @@ open Names
(* Utilities *)
+module Subscript =
+struct
+
+type t = {
+ ss_zero : int;
+ (** Number of leading zeros of the subscript *)
+ ss_subs : int;
+ (** Digital value of the subscript, zero meaning empty *)
+}
+
+let rec overflow n =
+ Int.equal (n mod 10) 9 && (Int.equal (n / 10) 0 || overflow (n / 10))
+
+let zero = { ss_subs = 0; ss_zero = 0 }
+
+let succ s =
+ if Int.equal s.ss_subs 0 then
+ if Int.equal s.ss_zero 0 then
+ (* [] -> [0] *)
+ { ss_zero = 1; ss_subs = 0 }
+ else
+ (* [0...00] -> [0..01] *)
+ { ss_zero = s.ss_zero - 1; ss_subs = 1 }
+ else if overflow s.ss_subs then
+ if Int.equal s.ss_zero 0 then
+ (* [9...9] -> [10...0] *)
+ { ss_zero = 0; ss_subs = 1 + s.ss_subs }
+ else
+ (* [0...009...9] -> [0...010...0] *)
+ { ss_zero = s.ss_zero - 1; ss_subs = 1 + s.ss_subs }
+ else
+ (* [0...0n] -> [0...0{n+1}] *)
+ { ss_zero = s.ss_zero; ss_subs = s.ss_subs + 1 }
+
+let equal s1 s2 =
+ Int.equal s1.ss_zero s2.ss_zero && Int.equal s1.ss_subs s2.ss_subs
+
+let compare s1 s2 =
+ (* Lexicographic order is reversed in order to ensure that [succ] is strictly
+ increasing. *)
+ let c = Int.compare s1.ss_subs s2.ss_subs in
+ if Int.equal c 0 then Int.compare s1.ss_zero s2.ss_zero else c
+
+end
+
let code_of_0 = Char.code '0'
let code_of_9 = Char.code '9'
@@ -104,6 +149,46 @@ let has_subscript id =
let id = Id.to_string id in
is_digit (id.[String.length id - 1])
+let get_subscript id =
+ let id0 = id in
+ let id = Id.to_string id in
+ let len = String.length id in
+ let rec get_suf accu pos =
+ if pos < 0 then (pos, accu)
+ else
+ let c = id.[pos] in
+ if is_digit c then get_suf (Char.code c - Char.code '0' :: accu) (pos - 1)
+ else (pos, accu)
+ in
+ let (pos, suf) = get_suf [] (len - 1) in
+ if Int.equal pos (len - 1) then (id0, Subscript.zero)
+ else
+ let id = String.sub id 0 (pos + 1) in
+ let rec compute_zeros accu = function
+ | [] -> (accu, [])
+ | 0 :: l -> compute_zeros (succ accu) l
+ | _ :: _ as l -> (accu, l)
+ in
+ let (ss_zero, suf) = compute_zeros 0 suf in
+ let rec compute_suf accu = function
+ | [] -> accu
+ | n :: l -> compute_suf (10 * accu + n) l
+ in
+ let ss_subs = compute_suf 0 suf in
+ (Id.of_string id, { Subscript.ss_subs; ss_zero; })
+
+let add_subscript id ss =
+ if Subscript.equal Subscript.zero ss then id
+ else if Int.equal ss.Subscript.ss_subs 0 then
+ let id = Id.to_string id in
+ let pad = String.make ss.Subscript.ss_zero '0' in
+ Id.of_string (Printf.sprintf "%s%s" id pad)
+ else
+ let id = Id.to_string id in
+ let pad = String.make ss.Subscript.ss_zero '0' in
+ let suf = ss.Subscript.ss_subs in
+ Id.of_string (Printf.sprintf "%s%s%i" id pad suf)
+
let forget_subscript id =
let numstart = cut_ident false id in
let newid = Bytes.make (numstart+1) '0' in
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 0e75fed045..222573450b 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -24,8 +24,42 @@ val add_prefix : string -> Id.t -> Id.t
(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *)
+module Subscript :
+sig
+ type t
+ (** Abstract datatype of subscripts. Isomorphic to a string of digits. *)
+
+ val zero : t
+ (** Empty subscript *)
+
+ val succ : t -> t
+ (** Guarantees that [x < succ x], but [succ x] might not be the smallest
+ element strictly above [x], generally it does not exist. Example mappings:
+ "" ↦ "0"
+ "0" ↦ "1"
+ "00" ↦ "01"
+ "1" ↦ "2"
+ "01" ↦ "02"
+ "9" ↦ "10"
+ "09" ↦ "10"
+ "99" ↦ "100"
+ *)
+
+ val compare : t -> t -> int
+ (** Well-founded order. *)
+
+ val equal : t -> t -> bool
+
+end
+
val has_subscript : Id.t -> bool
+val get_subscript : Id.t -> Id.t * Subscript.t
+(** Split an identifier into a base name and a subscript. *)
+
+val add_subscript : Id.t -> Subscript.t -> Id.t
+(** Append the subscript to the identifier. *)
+
val increment_subscript : Id.t -> Id.t
(** Return the same identifier as the original one but whose {i subscript} is incremented.
If the original identifier does not have a suffix, [0] is appended to it.
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2d693e0259..1fd8b5d50e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -345,29 +345,19 @@ let tclBREAK = Proof.break
exception NoSuchGoals of int
-(* This hook returns a string to be appended to the usual message.
- Primarily used to add a suggestion about the right bullet to use to
- focus the next goal, if applicable. *)
-let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ())
-let set_nosuchgoals_hook f = nosuchgoals_hook := f
-
-
-
-(* This uses the hook above *)
let _ = CErrors.register_handler begin function
| NoSuchGoals n ->
- let suffix = !nosuchgoals_hook n in
- CErrors.user_err
- (str "No such " ++ str (String.plural n "goal") ++ str "." ++
- pr_non_empty_arg (fun x -> x) suffix)
- | _ -> raise CErrors.Unhandled
+ CErrors.user_err
+ (str "No such " ++ str (String.plural n "goal") ++ str ".")
+ | _ -> raise CErrors.Unhandled
end
-(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where
+(** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where
only the goals numbered [i] to [j] are focused (the rest of the goals
is restored at the end of the tactic). If the range [i]-[j] is not
valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
-let tclFOCUS_gen nosuchgoal i j t =
+let tclFOCUS ?nosuchgoal i j t =
+ let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in
let open Proof in
Pv.get >>= fun initial ->
try
@@ -378,10 +368,9 @@ let tclFOCUS_gen nosuchgoal i j t =
return result
with CList.IndexOutOfRange -> nosuchgoal
-let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
-let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
+let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
-let tclFOCUSLIST l t =
+let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t =
let open Proof in
Comb.get >>= fun comb ->
let n = CList.length comb in
@@ -395,7 +384,7 @@ let tclFOCUSLIST l t =
in
let l = CList.map_filter sanitize l in
match l with
- | [] -> tclZERO (NoSuchGoals 0)
+ | [] -> nosuchgoal
| (mi, _) :: _ ->
(* Get the left-most goal to focus. This goal won't move, and we
will then place all the other goals to focus to the right. *)
@@ -412,7 +401,7 @@ let tclFOCUSLIST l t =
(** Like {!tclFOCUS} but selects a single goal by name. *)
-let tclFOCUSID id t =
+let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
let open Proof in
Pv.get >>= fun initial ->
try
@@ -432,7 +421,7 @@ let tclFOCUSID id t =
t >>= fun result ->
Comb.set initial.comb >>
return result
- with Not_found -> tclZERO (NoSuchGoals 1)
+ with Not_found -> nosuchgoal
(** {7 Dispatching on goals} *)
@@ -652,7 +641,7 @@ let shelve_goals l =
[sigma]. *)
let depends_on sigma src tgt =
let evi = Evd.find sigma tgt in
- Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
+ Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi))
let unifiable_delayed g l =
CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l
@@ -899,8 +888,8 @@ module Progress = struct
(** Equality function on goals *)
let goal_equal evars1 gl1 evars2 gl2 =
- let evi1 = Evd.find evars1 (drop_state gl1) in
- let evi2 = Evd.find evars2 (drop_state gl2) in
+ let evi1 = Evd.find evars1 gl1 in
+ let evi2 = Evd.find evars2 gl2 in
eq_evar_info evars1 evars2 evi1 evi2
end
@@ -918,7 +907,7 @@ let tclPROGRESS t =
let test =
quick_test ||
Util.List.for_all2eq begin fun i f ->
- Progress.goal_equal initial.solution i final.solution f
+ Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f)
end initial.comb final.comb
in
if not test then
@@ -1115,13 +1104,6 @@ module Goal = struct
tclZERO ~info e
end
end
-
- let normalize { self; state } =
- Env.get >>= fun env ->
- tclEVARMAP >>= fun sigma ->
- let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in
- tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
-
let gmake env sigma goal =
let state = get_state goal in
let goal = drop_state goal in
@@ -1269,9 +1251,9 @@ module V82 = struct
let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
{ Evd.it = goals ; sigma=solution; }
- let top_evars initial =
+ let top_evars initial { solution=sigma; } =
let evars_of_initial (c,_) =
- Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
+ Evar.Set.elements (Evd.evars_of_term sigma c)
in
CList.flatten (CList.map evars_of_initial initial)
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 680a93f0cc..b7ff3ac432 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -244,15 +244,12 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
(** [tclFOCUS i j t] applies [t] after focusing on the goals number
[i] to [j] (see {!focus}). The rest of the goals is restored after
the tactic action. If the specified range doesn't correspond to
- existing goals, fails with [NoSuchGoals] (a user error). this
- exception is caught at toplevel with a default message + a hook
- message that can be customized by [set_nosuchgoals_hook] below.
- This hook is used to add a suggestion about bullets when
- applicable. *)
+ existing goals, fails with the [nosuchgoal] argument, by default
+ raising [NoSuchGoals] (a user error). This exception is caught at
+ toplevel with a default message. *)
exception NoSuchGoals of int
-val set_nosuchgoals_hook: (int -> Pp.t) -> unit
-val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
+val tclFOCUS : ?nosuchgoal:'a tactic -> int -> int -> 'a tactic -> 'a tactic
(** [tclFOCUSLIST li t] applies [t] on the list of focused goals
described by [li]. Each element of [li] is a pair [(i, j)] denoting
@@ -261,13 +258,14 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
intervals. If the set of such goals is not a single range, then it
will move goals such that it is a single range. (So, for
instance, [[1, 3-5]; idtac.] is not the identity.)
- If the set of such goals is empty, it will fail. *)
-val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic
+ If the set of such goals is empty, it will fail with [nosuchgoal],
+ by default raising [NoSuchGoals 0]. *)
+val tclFOCUSLIST : ?nosuchgoal:'a tactic -> (int * int) list -> 'a tactic -> 'a tactic
(** [tclFOCUSID x t] applies [t] on a (single) focused goal like
{!tclFOCUS}. The goal is found by its name rather than its
- number.*)
-val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic
+ number. Fails with [nosuchgoal], by default raising [NoSuchGoals 1]. *)
+val tclFOCUSID : ?nosuchgoal:'a tactic -> Names.Id.t -> 'a tactic -> 'a tactic
(** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the
specified range doesn't correspond to existing goals, behaves like
@@ -395,10 +393,14 @@ val give_up : unit tactic
(** {7 Control primitives} *)
(** [tclPROGRESS t] checks the state of the proof after [t]. It it is
- identical to the state before, then [tclePROGRESS t] fails, otherwise
+ identical to the state before, then [tclPROGRESS t] fails, otherwise
it succeeds like [t]. *)
val tclPROGRESS : 'a tactic -> 'a tactic
+module Progress : sig
+ val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool
+end
+
(** Checks for interrupts *)
val tclCHECKINTERRUPT : unit tactic
@@ -503,10 +505,6 @@ module Goal : sig
(** Type of goals. *)
type t
- (** Normalises the argument goal. *)
- val normalize : t -> t tactic
- [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"]
-
(** [concl], [hyps], [env] and [sigma] given a goal [gl] return
respectively the conclusion of [gl], the hypotheses of [gl], the
environment of [gl] (i.e. the global environment and the
@@ -597,7 +595,7 @@ module V82 : sig
val top_goals : entry -> proofview -> Evar.t list Evd.sigma
(* returns the existential variable used to start the proof *)
- val top_evars : entry -> Evar.t list
+ val top_evars : entry -> proofview -> Evar.t list
(* Caution: this function loses quite a bit of information. It
should be avoided as much as possible. It should work as
diff --git a/engine/termops.ml b/engine/termops.ml
index 8e12c9be88..fcacb53ac4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -25,11 +25,6 @@ module CompactedDecl = Context.Compacted.Declaration
module Internal = struct
-let pr_sort_family = Sorts.pr_sort_family
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-let pr_fix = Constr.debug_print_fix
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c)
let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c)
let term_printer = ref debug_print_constr_env
@@ -192,7 +187,7 @@ let compute_evar_dependency_graph sigma =
in
match evar_body evi with
| Evar_empty -> acc
- | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc
+ | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term sigma c) acc
in
Evd.fold fold sigma EvMap.empty
@@ -761,13 +756,6 @@ let fold_constr_with_binders sigma g f n acc c =
let c = Unsafe.to_constr (whd_evar sigma c) in
Constr.fold_constr_with_binders g f n acc c
-(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
- subterms of [c]; it carries an extra data [acc] which is processed by [g] at
- each binder traversal; it is not recursive and the order with which
- subterms are processed is not specified *)
-
-let iter_constr_with_full_binders = EConstr.iter_with_full_binders
-
(***************************)
(* occurs check functions *)
(***************************)
@@ -862,8 +850,6 @@ let collect_vars sigma c =
| _ -> EConstr.fold sigma aux vars c in
aux Id.Set.empty c
-let vars_of_global_reference = vars_of_global
-
(* Tests whether [m] is a subterm of [t]:
[m] is appropriately lifted through abstractions of [t] *)
@@ -1417,10 +1403,6 @@ let prod_applist_assum sigma n c l =
| _ -> anomaly (Pp.str "Not enough prod/let's.") in
app n [] c l
-let on_judgment = Environ.on_judgment
-let on_judgment_value = Environ.on_judgment_value
-let on_judgment_type = Environ.on_judgment_type
-
(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
variables skips let-in's; let-in's in the middle are put in ctx2 *)
let context_chop k ctx =
diff --git a/engine/termops.mli b/engine/termops.mli
index 1dd9941c5e..a9217b3586 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -16,12 +16,6 @@ open Constr
open Environ
open EConstr
-(** printers *)
-val pr_sort_family : Sorts.family -> Pp.t
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
(** about contexts *)
val push_rel_assum : Name.t Context.binder_annot * types -> env -> env
val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env
@@ -84,12 +78,6 @@ val fold_constr_with_full_binders : Evd.evar_map ->
('a -> 'b -> constr -> 'b) ->
'a -> 'b -> constr -> 'b
-val iter_constr_with_full_binders : Evd.evar_map ->
- (rel_declaration -> 'a -> 'a) ->
- ('a -> constr -> unit) -> 'a ->
- constr -> unit
-[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."]
-
(**********************************************************************)
val strip_head_cast : Evd.evar_map -> constr -> constr
@@ -121,9 +109,6 @@ val count_occurrences : Evd.evar_map -> constr -> constr -> int
val collect_metas : Evd.evar_map -> constr -> int list
val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
-val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
-[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
-
(* Substitution of metavariables *)
type meta_value_map = (metavariable * Constr.constr) list
val subst_meta : meta_value_map -> Constr.constr -> Constr.constr
@@ -292,15 +277,6 @@ val is_Type : Evd.evar_map -> constr -> bool
val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
-(** Combinators on judgments *)
-
-val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment]."]
-val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_value]."]
-val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_type]."]
-
(** {5 Debug pretty-printers} *)
open Evd
diff --git a/engine/uState.ml b/engine/uState.ml
index 6f4f40e2c5..adea78d4c9 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -85,7 +85,7 @@ let union ctx ctx' =
let declarenew g =
LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
in
- let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
+ let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in
{ uctx_names = (names, names_rev);
uctx_local = local;
uctx_seff_univs = seff;
@@ -116,8 +116,6 @@ let univ_entry ~poly uctx =
Polymorphic_entry (nas, uctx)
else Monomorphic_entry (context_set uctx)
-let const_univ_entry = univ_entry
-
let of_context_set ctx = { empty with uctx_local = ctx }
let subst ctx = ctx.uctx_univ_variables
diff --git a/engine/uState.mli b/engine/uState.mli
index a358813825..3df7f9e8e9 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -67,9 +67,6 @@ val context : t -> Univ.UContext.t
val univ_entry : poly:bool -> t -> Entries.universes_entry
(** Pick from {!context} or {!context_set} based on [poly]. *)
-val const_univ_entry : poly:bool -> t -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
(** {5 Constraints handling} *)
val drop_weak_constraints : bool ref
diff --git a/engine/univGen.ml b/engine/univGen.ml
index c310331b15..f1deb1bfaf 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -25,11 +25,6 @@ let new_univ_global () =
let fresh_level () =
Univ.Level.make (new_univ_global ())
-(* TODO: remove *)
-let new_univ () = Univ.Universe.make (fresh_level ())
-let new_Type () = mkType (new_univ ())
-let new_Type_sort () = sort_of_univ (new_univ ())
-
let fresh_instance auctx =
let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
let ctx = Array.fold_right LSet.add inst LSet.empty in
@@ -83,10 +78,6 @@ let constr_of_monomorphic_global gr =
Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
str " would forget universes.")
-let constr_of_global gr = constr_of_monomorphic_global gr
-
-let constr_of_global_univ = mkRef
-
let fresh_global_or_constr_instance env = function
| IsConstr c -> c, ContextSet.empty
| IsGlobal gr -> fresh_global_instance env gr
@@ -99,34 +90,6 @@ let global_of_constr c =
| Var id -> VarRef id, Instance.empty
| _ -> raise Not_found
-open Declarations
-
-let type_of_reference env r =
- match r with
- | VarRef id -> Environ.named_type id env, ContextSet.empty
-
- | ConstRef c ->
- let cb = Environ.lookup_constant c env in
- let ty = cb.const_type in
- let auctx = Declareops.constant_polymorphic_context cb in
- let inst, ctx = fresh_instance auctx in
- Vars.subst_instance_constr inst ty, ctx
-
- | IndRef ind ->
- let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
- let auctx = Declareops.inductive_polymorphic_context mib in
- let inst, ctx = fresh_instance auctx in
- let ty = Inductive.type_of_inductive env (specif, inst) in
- ty, ctx
-
- | ConstructRef (ind,_ as cstr) ->
- let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- let auctx = Declareops.inductive_polymorphic_context mib in
- let inst, ctx = fresh_instance auctx in
- Inductive.type_of_constructor (cstr,inst) specif, ctx
-
-let type_of_global t = type_of_reference (Global.env ()) t
-
let fresh_sort_in_family = function
| InSProp -> Sorts.sprop, ContextSet.empty
| InProp -> Sorts.prop, ContextSet.empty
@@ -135,11 +98,6 @@ let fresh_sort_in_family = function
let u = fresh_level () in
sort_of_univ (Univ.Universe.make u), ContextSet.singleton u
-let new_sort_in_family sf =
- fst (fresh_sort_in_family sf)
-
-let extend_context = Univ.extend_in_context_set
-
let new_global_univ () =
let u = fresh_level () in
(Univ.Universe.make u, ContextSet.singleton u)
diff --git a/engine/univGen.mli b/engine/univGen.mli
index b4598e10d0..34920e5620 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -24,16 +24,7 @@ val new_univ_id : unit -> univ_unique_id (** for the stm *)
val new_univ_global : unit -> Level.UGlobal.t
val fresh_level : unit -> Level.t
-val new_univ : unit -> Universe.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type : unit -> types
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type_sort : unit -> Sorts.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-
val new_global_univ : unit -> Universe.t in_universe_context_set
-val new_sort_in_family : Sorts.family -> Sorts.t
-[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
(** Build a fresh instance for a given context, its associated substitution and
the instantiated constraints. *)
@@ -66,27 +57,9 @@ val fresh_universe_context_set_instance : ContextSet.t ->
(** Raises [Not_found] if not a global reference. *)
val global_of_constr : constr -> GlobRef.t puniverses
-val constr_of_global_univ : GlobRef.t puniverses -> constr
-[@@ocaml.deprecated "Use [Constr.mkRef]"]
-
-val extend_context : 'a in_universe_context_set -> ContextSet.t ->
- 'a in_universe_context_set
-[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
-
(** Create a fresh global in the global environment, without side effects.
BEWARE: this raises an error on polymorphic constants/inductives:
the constraints should be properly added to an evd.
See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
the proper way to get a fresh copy of a polymorphic global reference. *)
val constr_of_monomorphic_global : GlobRef.t -> constr
-
-val constr_of_global : GlobRef.t -> constr
-[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\
- use [constr_of_monomorphic_global] if the reference is guaranteed to\
- be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"]
-
-(** Returns the type of the global reference, by creating a fresh instance of polymorphic
- references and computing their instantiated universe context. (side-effect on the
- universe counter, use with care). *)
-val type_of_global : GlobRef.t -> types in_universe_context_set
-[@@ocaml.deprecated "use [Typeops.type_of_global]"]
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 46ff6340b4..fcbf305f9d 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -203,7 +203,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
(acc, [], LMap.empty, LMap.empty) l
in
let left = CList.uniquize (List.filter (not_lower lower) left) in
- (acc, left, LMap.union newlow lower)
+ (acc, left, LMap.lunion newlow lower)
in
let instantiate_lbound lbound =
let alg = LSet.mem u algs in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:38:45 +0000