aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/eqschemes.ml24
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/hints.ml18
-rw-r--r--tactics/ind_tables.ml4
-rw-r--r--tactics/tactics.ml26
-rw-r--r--tactics/tactics.mli4
10 files changed, 34 insertions, 56 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 15a24fb37a..77fe314150 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -79,7 +79,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
let clenv, c =
if poly then
(** Refresh the instance of the hint *)
- let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+ let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let emap c = Vars.subst_univs_level_constr subst c in
let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
(** Only metas are mentioning the old universes. *)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c3857e6b8b..0b0e629ab5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -30,7 +30,7 @@ let subst_hint subst hint =
let cst' = subst_mps subst hint.rew_lemma in
let typ' = subst_mps subst hint.rew_type in
let pat' = subst_mps subst hint.rew_pat in
- let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in
+ let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in
if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
{ hint with
rew_lemma = cst'; rew_type = typ';
@@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
let try_rewrite dir ctx c tc =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
- let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+ let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in
let c' = Vars.subst_univs_level_constr subst c in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index bbcf8def6d..ea5d4719c1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -226,7 +226,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
Refine.refine ~typecheck:false begin fun sigma ->
let sigma, term, ty =
if poly then
- let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+ let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let map c = Vars.subst_univs_level_constr subst c in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
sigma, map c, map t
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2408b8f2b2..3df9e3f820 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -89,7 +89,7 @@ let rec prolog l n gl =
let out_term env = function
| IsConstr (c, _) -> c
- | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
+ | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr))
let prolog_tac l n =
Proofview.V82.tactic begin fun gl ->
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 477de6452e..715686ad03 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -102,7 +102,7 @@ let get_coq_eq ctx =
let eq = Globnames.destIndRef Coqlib.glob_eq in
(* Do not force the lazy if they are not defined *)
let eq, ctx = with_context_set ctx
- (Universes.fresh_inductive_instance (Global.env ()) eq) in
+ (UnivGen.fresh_inductive_instance (Global.env ()) eq) in
mkIndU eq, mkConstructUi (eq,1), ctx
with Not_found ->
user_err Pp.(str "eq not found.")
@@ -192,7 +192,7 @@ let get_non_sym_eq_data env (ind,u) =
(**********************************************************************)
let build_sym_scheme env ind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let cstr n =
@@ -241,11 +241,11 @@ let sym_scheme_kind =
let const_of_scheme kind env ind ctx =
let sym_scheme, eff = (find_scheme kind ind) in
let sym, ctx = with_context_set ctx
- (Universes.fresh_constant_instance (Global.env()) sym_scheme) in
+ (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
mkConstU sym, ctx, eff
let build_sym_involutive_scheme env ind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let eq,eqrefl,ctx = get_coq_eq ctx in
@@ -353,7 +353,7 @@ let sym_involutive_scheme_kind =
(**********************************************************************)
let build_l2r_rew_scheme dep env ind kind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
@@ -392,7 +392,7 @@ let build_l2r_rew_scheme dep env ind kind =
rel_vect (nrealargs+4) nrealargs;
rel_vect 1 nrealargs;
[|mkRel 1|]]) in
- let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+ let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -469,7 +469,7 @@ let build_l2r_rew_scheme dep env ind kind =
(**********************************************************************)
let build_l2r_forward_rew_scheme dep env ind kind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let cstr n p =
@@ -495,7 +495,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
let realsign_ind_P n aP =
name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in
- let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+ let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -561,7 +561,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(**********************************************************************)
let build_r2l_forward_rew_scheme dep env ind kind =
- let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+ let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
get_non_sym_eq_data env indu in
let cstr n =
@@ -573,7 +573,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
let applied_ind = build_dependent_inductive indu specif in
let realsign_ind =
name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
- let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+ let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
let ctx = Univ.ContextSet.union ctx ctx' in
let s = mkSort s in
let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -755,7 +755,7 @@ let rew_r2l_scheme_kind =
let build_congr env (eq,refl,ctx) ind =
let (ind,u as indu), ctx = with_context_set ctx
- (Universes.fresh_inductive_instance env ind) in
+ (UnivGen.fresh_inductive_instance env ind) in
let (mib,mip) = lookup_mind_specif env ind in
if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then
error "Not an inductive type with a single constructor.";
@@ -778,7 +778,7 @@ let build_congr env (eq,refl,ctx) ind =
let varH = fresh env (Id.of_string "H") in
let varf = fresh env (Id.of_string "f") in
let ci = make_case_info (Global.env()) ind RegularStyle in
- let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in
+ let uni, ctx = UnivGen.extend_context (UnivGen.new_global_univ ()) ctx in
let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
let c =
my_it_mkLambda_or_LetIn paramsctxt
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d142e10a4f..8904cd170b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1781,7 +1781,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
let u = EInstance.kind sigma u in
- let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+ let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
match EConstr.kind sigma x, EConstr.kind sigma y with
| Var z, _ when not (is_evaluable env (EvalVarRef z)) ->
@@ -1832,7 +1832,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose c in
let u = EInstance.kind sigma u in
- let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+ let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if EConstr.eq_constr sigma x y then failwith "caught";
diff --git a/tactics/hints.ml b/tactics/hints.ml
index d02bab1864..3ade5314b9 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -448,7 +448,7 @@ let subst_path_atom subst p =
| PathAny -> p
| PathHints grs ->
let gr' gr = fst (subst_global subst gr) in
- let grs' = List.smartmap gr' grs in
+ let grs' = List.Smart.map gr' grs in
if grs' == grs then p else PathHints grs'
let rec subst_hints_path subst hp =
@@ -654,7 +654,7 @@ struct
let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l
- let remove_sdl p sdl = List.smartfilter p sdl
+ let remove_sdl p sdl = List.Smart.filter p sdl
let remove_he st p se =
let sl1' = remove_sdl p se.sentry_nopat in
@@ -666,7 +666,7 @@ struct
let filter (_, h) =
match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
- let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
+ let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
{ db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
let remove_one gr db = remove_list [gr] db
@@ -876,7 +876,7 @@ let fresh_global_or_constr env sigma poly cr =
let isgr, (c, ctx) =
match cr with
| IsGlobRef gr ->
- let (c, ctx) = Universes.fresh_global_instance env gr in
+ let (c, ctx) = UnivGen.fresh_global_instance env gr in
true, (EConstr.of_constr c, ctx)
| IsConstr (c, ctx) -> false, (c, ctx)
in
@@ -1065,8 +1065,8 @@ let subst_autohint (subst, obj) =
in if gr' == gr then gr else gr'
in
let subst_hint (k,data as hint) =
- let k' = Option.smartmap subst_key k in
- let pat' = Option.smartmap (subst_pattern subst) data.pat in
+ let k' = Option.Smart.map subst_key k in
+ let pat' = Option.Smart.map (subst_pattern subst) data.pat in
let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
let code' = match data.code.obj with
| Res_pf (c,t,ctx) ->
@@ -1104,13 +1104,13 @@ let subst_autohint (subst, obj) =
let action = match obj.hint_action with
| CreateDB _ -> obj.hint_action
| AddTransparency (grs, b) ->
- let grs' = List.smartmap (subst_evaluable_reference subst) grs in
+ let grs' = List.Smart.map (subst_evaluable_reference subst) grs in
if grs == grs' then obj.hint_action else AddTransparency (grs', b)
| AddHints hintlist ->
- let hintlist' = List.smartmap subst_hint hintlist in
+ let hintlist' = List.Smart.map subst_hint hintlist in
if hintlist' == hintlist then obj.hint_action else AddHints hintlist'
| RemoveHints grs ->
- let grs' = List.smartmap (subst_global_reference subst) grs in
+ let grs' = List.Smart.map (subst_global_reference subst) grs in
if grs == grs' then obj.hint_action else RemoveHints grs'
| AddCut path ->
let path' = subst_hints_path subst path in
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 62ead57f38..21520f5d2b 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -53,7 +53,7 @@ let subst_one_scheme subst (ind,const) =
(subst_ind subst ind,subst_constant subst const)
let subst_scheme (subst,(kind,l)) =
- (kind,Array.map (subst_one_scheme subst) l)
+ (kind,Array.Smart.map (subst_one_scheme subst) l)
let discharge_scheme (_,(kind,l)) =
Some (kind,Array.map (fun (ind,const) ->
@@ -123,7 +123,7 @@ let define internal id c p univs =
let fd = declare_constant ~internal in
let id = compute_name internal id in
let ctx = UState.minimize univs in
- let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in
+ let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
let univs =
if p then Polymorphic_const_entry (UState.context ctx)
else Monomorphic_const_entry (UState.context_set ctx)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 01351e2492..a42e4b44b5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -563,20 +563,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
end
end
-let warning_nameless_fix =
- CWarnings.create ~name:"nameless-fix" ~category:"deprecated" Pp.(fun () ->
- str "fix/cofix without a name are deprecated, please use the named version.")
-
-let fix ido n = match ido with
- | None ->
- warning_nameless_fix ();
- Proofview.Goal.enter begin fun gl ->
- let name = Proof_global.get_current_proof_name () in
- let id = new_fresh_id Id.Set.empty name gl in
- mutual_fix id n [] 0
- end
- | Some id ->
- mutual_fix id n [] 0
+let fix id n = mutual_fix id n [] 0
let rec check_is_mutcoind env sigma cl =
let b = whd_all env sigma cl in
@@ -619,16 +606,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl ->
end
end
-let cofix ido = match ido with
- | None ->
- warning_nameless_fix ();
- Proofview.Goal.enter begin fun gl ->
- let name = Proof_global.get_current_proof_name () in
- let id = new_fresh_id Id.Set.empty name gl in
- mutual_cofix id [] 0
- end
- | Some id ->
- mutual_cofix id [] 0
+let cofix id = mutual_cofix id [] 0
(**************************************************************)
(* Reduction and conversion tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 46f782eaa5..ddf78b1d4e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -41,9 +41,9 @@ val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
-val fix : Id.t option -> int -> unit Proofview.tactic
+val fix : Id.t -> int -> unit Proofview.tactic
val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic
-val cofix : Id.t option -> unit Proofview.tactic
+val cofix : Id.t -> unit Proofview.tactic
val convert : constr -> constr -> unit Proofview.tactic
val convert_leq : constr -> constr -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 19:40:26 +0000