aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/autorewrite.ml3
-rw-r--r--tactics/autorewrite.mli6
-rw-r--r--tactics/elimschemes.ml3
-rw-r--r--tactics/elimschemes.mli2
-rw-r--r--tactics/eqschemes.ml7
-rw-r--r--tactics/eqschemes.mli12
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/hints.ml4
-rw-r--r--tactics/hints.mli8
-rw-r--r--tactics/ind_tables.ml6
-rw-r--r--tactics/ind_tables.mli10
-rw-r--r--tactics/tacticals.ml11
-rw-r--r--tactics/tacticals.mli14
-rw-r--r--tactics/tactics.ml15
-rw-r--r--tactics/tactics.mli2
-rw-r--r--tactics/term_dnet.ml6
-rw-r--r--tactics/term_dnet.mli2
17 files changed, 60 insertions, 57 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ed612c0fc9..e68087f140 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -10,6 +10,7 @@ open Equality
open Names
open Pp
open Term
+open Constr
open Termops
open CErrors
open Util
@@ -20,7 +21,7 @@ open Locus
type rew_rule = { rew_lemma: constr;
rew_type: types;
rew_pat: constr;
- rew_ctx: Univ.universe_context_set;
+ rew_ctx: Univ.ContextSet.t;
rew_l2r: bool;
rew_tac: Genarg.glob_generic_argument option }
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index edbb7c6b71..d2b5e070bd 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -8,7 +8,7 @@
(** This files implements the autorewrite tactic. *)
-open Term
+open Constr
open Equality
(** Rewriting rules before tactic interpretation *)
@@ -28,7 +28,7 @@ val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic ->
type rew_rule = { rew_lemma: constr;
rew_type: types;
rew_pat: constr;
- rew_ctx: Univ.universe_context_set;
+ rew_ctx: Univ.ContextSet.t;
rew_l2r: bool;
rew_tac: Genarg.glob_generic_argument option }
@@ -58,5 +58,5 @@ type hypinfo = {
val find_applied_relation :
?loc:Loc.t -> bool ->
- Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo
+ Environ.env -> Evd.evar_map -> constr -> bool -> hypinfo
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 2d2a0c1b2a..e427adb15d 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -13,7 +13,8 @@
(* This file builds schemes related to case analysis and recursion schemes *)
-open Term
+open Sorts
+open Constr
open Indrec
open Declarations
open Typeops
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index e3fe7ddae9..9c750e7ad1 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -13,7 +13,7 @@ open Ind_tables
val optimize_non_type_induction_scheme :
'a Ind_tables.scheme_kind ->
Indrec.dep_flag ->
- Term.sorts_family ->
+ Sorts.family ->
'b ->
Names.inductive ->
(Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index bfbac77872..d7667668e8 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -48,6 +48,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open Vars
open Declarations
open Environ
@@ -106,8 +107,8 @@ let get_coq_eq ctx =
let univ_of_eq env eq =
let eq = EConstr.of_constr eq in
- match kind_of_term (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
- | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false)
+ match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
+ | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false)
| _ -> assert false
(**********************************************************************)
@@ -141,7 +142,7 @@ let get_sym_eq_data env (ind,u) =
let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in
let paramsctxt1,_ =
List.chop (mib.mind_nparams-mip.mind_nrealargs) paramsctxt in
- if not (List.equal Term.eq_constr params2 constrargs) then
+ if not (List.equal Constr.equal params2 constrargs) then
error "Constructors arguments must repeat the parameters.";
(* nrealargs_ctxt and nrealargs are the same here *)
(specif,mip.mind_nrealargs,realsign,paramsctxt,paramsctxt1)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 4acfa7a281..90ae67c6cf 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -9,7 +9,7 @@
(** This file builds schemes relative to equality inductive types *)
open Names
-open Term
+open Constr
open Environ
open Ind_tables
@@ -22,14 +22,14 @@ val rew_l2r_forward_dep_scheme_kind : individual scheme_kind
val rew_r2l_dep_scheme_kind : individual scheme_kind
val rew_r2l_scheme_kind : individual scheme_kind
-val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family ->
+val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family ->
constr Evd.in_evar_universe_context
-val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family ->
+val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family ->
constr Evd.in_evar_universe_context * Safe_typing.private_constants
val build_r2l_forward_rew_scheme :
- bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context
+ bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
val build_l2r_forward_rew_scheme :
- bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context
+ bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
(** Builds a symmetry scheme for a symmetrical equality type *)
@@ -43,5 +43,5 @@ val sym_involutive_scheme_kind : individual scheme_kind
(** Builds a congruence scheme for an equality type *)
val congr_scheme_kind : individual scheme_kind
-val build_congr : env -> constr * constr * Univ.universe_context_set -> inductive ->
+val build_congr : env -> constr * constr * Univ.ContextSet.t -> inductive ->
constr Evd.in_evar_universe_context
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7c03a3ba6a..881000219c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -374,16 +374,16 @@ let find_elim hdcncl lft2rgt dep cls ot =
| Some true, None
| Some false, Some _ ->
let c1 = destConstRef pr1 in
- let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in
+ let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical c1)) in
let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in
- let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in
+ let c1' = Global.constant_of_delta_kn (KerName.make mp dp l') in
begin
try
let _ = Global.lookup_constant c1' in
c1'
with Not_found ->
user_err ~hdr:"Equality.find_elim"
- (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
+ (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
end
| _ -> destConstRef pr1
end
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3ccbab874f..c7c53b3930 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -128,14 +128,14 @@ type hints_path = global_reference hints_path_gen
type hint_term =
| IsGlobRef of global_reference
- | IsConstr of constr * Univ.universe_context_set
+ | IsConstr of constr * Univ.ContextSet.t
type 'a with_uid = {
obj : 'a;
uid : KerName.t;
}
-type raw_hint = constr * types * Univ.universe_context_set
+type raw_hint = constr * types * Univ.ContextSet.t
type hint = (raw_hint * clausenv) hint_ast with_uid
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 44e5370e93..22df29b803 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -42,7 +42,7 @@ type 'a hint_ast =
| Extern of Genarg.glob_generic_argument (* Hint Extern *)
type hint
-type raw_hint = constr * types * Univ.universe_context_set
+type raw_hint = constr * types * Univ.ContextSet.t
type 'a hints_path_atom_gen =
| PathHints of 'a list
@@ -146,7 +146,7 @@ type hint_info = (patvar list * constr_pattern) hint_info_gen
type hint_term =
| IsGlobRef of global_reference
- | IsConstr of constr * Univ.universe_context_set
+ | IsConstr of constr * Univ.ContextSet.t
type hints_entry =
| HintsResolveEntry of
@@ -193,7 +193,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
*)
val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom ->
- (constr * types * Univ.universe_context_set) -> hint_entry
+ (constr * types * Univ.ContextSet.t) -> hint_entry
(** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
[eapply] is true if this hint will be used only with EApply;
@@ -211,7 +211,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hint
val make_apply_entry :
env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
- (constr * types * Univ.universe_context_set) -> hint_entry
+ (constr * types * Univ.ContextSet.t) -> hint_entry
(** A constr which is Hint'ed will be:
- (1) used as an Exact, if it does not start with a product
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 7f087ea01a..e7fa555c2b 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -17,7 +17,7 @@ open Mod_subst
open Libobject
open Nameops
open Declarations
-open Term
+open Constr
open CErrors
open Util
open Declare
@@ -29,7 +29,7 @@ open Pp
(* Registering schemes in the environment *)
type mutual_scheme_object_function =
- internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+ internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
type individual_scheme_object_function =
internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
@@ -57,7 +57,7 @@ let discharge_scheme (_,(kind,l)) =
Some (kind,Array.map (fun (ind,const) ->
(Lib.discharge_inductive ind,Lib.discharge_con const)) l)
-let inScheme : string * (inductive * constant) array -> obj =
+let inScheme : string * (inductive * Constant.t) array -> obj =
declare_object {(default_object "SCHEME") with
cache_function = cache_scheme;
load_function = (fun _ -> cache_scheme);
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index f825c4f4a3..d73595a2f8 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -6,8 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
open Names
+open Constr
open Declare
(** This module provides support for registering inductive scheme builders,
@@ -20,7 +20,7 @@ type individual
type 'a scheme_kind
type mutual_scheme_object_function =
- internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+ internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
type individual_scheme_object_function =
internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
@@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string ->
val define_individual_scheme : individual scheme_kind ->
internal_flag (** internal *) ->
- Id.t option -> inductive -> constant * Safe_typing.private_constants
+ Id.t option -> inductive -> Constant.t * Safe_typing.private_constants
val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
- (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants
+ (int * Id.t) list -> MutInd.t -> Constant.t array * Safe_typing.private_constants
(** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants
val check_scheme : 'a scheme_kind -> inductive -> bool
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 07eea7b63e..cea6ccc303 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -10,7 +10,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open EConstr
open Termops
open Declarations
@@ -224,9 +224,8 @@ let compute_induction_names = compute_induction_names_gen true
(* Compute the let-in signature of case analysis or standard induction scheme *)
let compute_constructor_signatures isrec ((_,k as ity),u) =
- let open Term in
let rec analrec c recargs =
- match kind_of_term c, recargs with
+ match Constr.kind c, recargs with
| Prod (_,_,c), recarg::rest ->
let rest = analrec c rest in
begin match Declareops.dest_recarg recarg with
@@ -242,7 +241,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
let (mib,mip) = Global.lookup_inductive ity in
let n = mib.mind_nparams in
let lc =
- Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in
+ Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in
let lrecargs = Declareops.dest_subterms mip.mind_recargs in
Array.map2 analrec lc lrecargs
@@ -472,7 +471,7 @@ module New = struct
let evi = Evd.find sigma evk in
match Evd.evar_body evi with
| Evd.Evar_empty -> Some (evk,evi)
- | Evd.Evar_defined c -> match Term.kind_of_term c with
+ | Evd.Evar_defined c -> match Constr.kind c with
| Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk
| _ ->
(* We make the assumption that there is no way to refine an
@@ -622,7 +621,7 @@ module New = struct
| _ ->
let name_elim =
match EConstr.kind sigma elim with
- | Const (kn, _) -> string_of_con kn
+ | Const (kn, _) -> Constant.to_string kn
| Var id -> Id.to_string id
| _ -> "\b"
in
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3abd42d46a..f5c209c74b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open EConstr
open Tacmach
open Proof_type
@@ -127,9 +127,9 @@ val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list arr
val compute_induction_names :
bool list array -> or_and_intro_pattern option -> intro_patterns array
-val elimination_sort_of_goal : goal sigma -> sorts_family
-val elimination_sort_of_hyp : Id.t -> goal sigma -> sorts_family
-val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family
+val elimination_sort_of_goal : goal sigma -> Sorts.family
+val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family
+val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family
val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
@@ -243,9 +243,9 @@ module New : sig
val tryAllHypsAndConcl : (Id.t option -> unit tactic) -> unit tactic
val onClause : (Id.t option -> unit tactic) -> clause -> unit tactic
- val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family
- val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> sorts_family
- val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> sorts_family
+ val elimination_sort_of_goal : 'a Proofview.Goal.t -> Sorts.family
+ val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> Sorts.family
+ val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> Sorts.family
val elimination_then :
(branch_args -> unit Proofview.tactic) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f67606d24..ba244a794e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -14,6 +14,7 @@ open Util
open Names
open Nameops
open Term
+open Constr
open Termops
open Environ
open EConstr
@@ -580,7 +581,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
| (f, n, ar) :: oth ->
let open Context.Named.Declaration in
let (sp', u') = check_mutind env sigma n ar in
- if not (eq_mind sp sp') then
+ if not (MutInd.equal sp sp') then
error "Fixpoints should be on the same mutual inductive declaration.";
if mem_named_context_val f sign then
user_err ~hdr:"Logic.prim_refiner"
@@ -1290,7 +1291,7 @@ let check_unresolved_evars_of_metas sigma clenv =
(* Refiner.pose_all_metas_as_evars are resolved *)
List.iter (fun (mv,b) -> match b with
| Clval (_,(c,_),_) ->
- (match kind_of_term c.rebus with
+ (match Constr.kind c.rebus with
| Evar (evk,_) when Evd.is_undefined clenv.evd evk
&& not (Evd.mem sigma evk) ->
error_uninstantiated_metas (mkMeta mv) clenv
@@ -1607,7 +1608,7 @@ let general_elim_clause with_evars flags id c e =
(* Apply a tactic below the products of the conclusion of a lemma *)
type conjunction_status =
- | DefinedRecord of constant option list
+ | DefinedRecord of Constant.t option list
| NotADefinedRecordUseScheme of constr
let make_projection env sigma params cstr sign elim i n c u =
@@ -4958,7 +4959,7 @@ let interpretable_as_section_decl evd d1 d2 =
let rec decompose len c t accu =
let open Context.Rel.Declaration in
if len = 0 then (c, t, accu)
- else match kind_of_term c, kind_of_term t with
+ else match Constr.kind c, Constr.kind t with
| Lambda (na, u, c), Prod (_, _, t) ->
decompose (pred len) c t (LocalAssum (na, u) :: accu)
| LetIn (na, b, u, c), LetIn (_, _, _, t) ->
@@ -4966,7 +4967,7 @@ let rec decompose len c t accu =
| _ -> assert false
let rec shrink ctx sign c t accu =
- let open Term in
+ let open Constr in
let open CVars in
match ctx, sign with
| [], [] -> (c, t, accu)
@@ -4976,8 +4977,8 @@ let rec shrink ctx sign c t accu =
let t = subst1 mkProp t in
shrink ctx sign c t accu
else
- let c = mkLambda_or_LetIn p c in
- let t = mkProd_or_LetIn p t in
+ let c = Term.mkLambda_or_LetIn p c in
+ let t = Term.mkProd_or_LetIn p t in
let accu = if RelDecl.is_local_assum p
then mkVar (NamedDecl.get_id decl) :: accu
else accu
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 98cf1b4373..83fc655f1c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -8,7 +8,7 @@
open Loc
open Names
-open Term
+open Constr
open EConstr
open Environ
open Proof_type
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 64ba38a51b..6c8130d793 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -8,7 +8,7 @@
(*i*)
open Util
-open Term
+open Constr
open Names
open Globnames
open Mod_subst
@@ -257,7 +257,7 @@ struct
let pat_of_constr c : term_pattern =
(** To each evar we associate a unique identifier. *)
let metas = ref Evar.Map.empty in
- let rec pat_of_constr c = match kind_of_term c with
+ let rec pat_of_constr c = match Constr.kind c with
| Rel _ -> Term DRel
| Sort _ -> Term DSort
| Var i -> Term (DRef (VarRef i))
@@ -290,7 +290,7 @@ struct
| Proj (p,c) ->
Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c))
- and ctx_of_constr ctx c = match kind_of_term c with
+ and ctx_of_constr ctx c = match Constr.kind c with
| Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c
| LetIn(_,d,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t, Some (pat_of_constr d)),ctx))) c
| _ -> ctx,pat_of_constr c
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index 16122fa5e0..db7da18ba9 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
+open Constr
open Mod_subst
(** Dnets on constr terms.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 12:15:31 +0000