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/eauto.ml4
-rw-r--r--tactics/elimschemes.ml3
-rw-r--r--tactics/elimschemes.mli4
-rw-r--r--tactics/eqschemes.ml7
-rw-r--r--tactics/eqschemes.mli12
-rw-r--r--tactics/equality.ml12
-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/inv.ml5
-rw-r--r--tactics/tacticals.ml11
-rw-r--r--tactics/tacticals.mli17
-rw-r--r--tactics/tactics.ml75
-rw-r--r--tactics/tactics.mli2
-rw-r--r--tactics/term_dnet.ml6
-rw-r--r--tactics/term_dnet.mli2
19 files changed, 100 insertions, 97 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/eauto.ml b/tactics/eauto.ml
index 9097aebd01..239661498b 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -10,13 +10,13 @@ open Pp
open CErrors
open Util
open Names
-open Nameops
open Term
open Termops
open EConstr
open Proof_type
open Tacticals
open Tacmach
+open Evd
open Tactics
open Clenv
open Auto
@@ -261,7 +261,7 @@ module SearchProblem = struct
let g = find_first_goal lg in
let hyps = pf_ids_of_hyps g in
let secvars = secvars_of_hyps (pf_hyps g) in
- let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
+ let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ Id.print id)) in
let assumption_tacs =
let tacs = List.map map_assum hyps in
let l = filter_tactics s.tacres tacs in
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..50b052f23b 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -13,10 +13,10 @@ 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
+ (Constr.constr * UState.t) * Safe_typing.private_constants
val rect_scheme_kind_from_prop : individual scheme_kind
val ind_scheme_kind_from_prop : individual scheme_kind
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..c36ad980ef 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
@@ -1760,7 +1760,7 @@ let subst_one_var dep_proof_ok x =
let test hyp _ = is_eq_x gl x hyp in
Context.Named.fold_outside test ~init:() hyps;
user_err ~hdr:"Subst"
- (str "Cannot find any non-recursive equality over " ++ pr_id x ++
+ (str "Cannot find any non-recursive equality over " ++ Id.print x ++
str".")
with FoundHyp res -> res in
subst_one dep_proof_ok x res
@@ -1824,9 +1824,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
match EConstr.kind sigma x, EConstr.kind sigma y with
- | Var x', _ when not (occur_term sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
+ | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
- | _, Var y' when not (occur_term sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
+ | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
| _ ->
Proofview.tclUNIT ()
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/inv.ml b/tactics/inv.ml
index c5aa74ba5c..8648dfb90c 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -10,7 +10,6 @@ open Pp
open CErrors
open Util
open Names
-open Nameops
open Term
open Termops
open EConstr
@@ -78,7 +77,7 @@ let make_inv_predicate env evd indf realargs id status concl =
| Dep dflt_concl ->
if not (occur_var env !evd id concl) then
user_err ~hdr:"make_inv_predicate"
- (str "Current goal does not depend on " ++ pr_id id ++ str".");
+ (str "Current goal does not depend on " ++ Id.print id ++ str".");
(* We abstract the conclusion of goal with respect to
realargs and c to * be concl in order to rewrite and have
c also rewritten when the case * will be done *)
@@ -442,7 +441,7 @@ let raw_inversion inv_kind id status names =
let (ind, t) =
try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
with UserError _ ->
- let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
+ let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in
CErrors.user_err msg
in
let IndType (indf,realargs) = find_rectype env sigma t in
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..169ac5c90d 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -7,9 +7,9 @@
(************************************************************************)
open Names
-open Term
+open Constr
open EConstr
-open Tacmach
+open Evd
open Proof_type
open Locus
open Misctypes
@@ -23,6 +23,7 @@ val tclORELSE0 : tactic -> tactic -> tactic
val tclORELSE : tactic -> tactic -> tactic
val tclTHEN : tactic -> tactic -> tactic
val tclTHENSEQ : tactic list -> tactic
+[@@ocaml.deprecated "alias of API.Tacticals.tclTHENLIST"]
val tclTHENLIST : tactic list -> tactic
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
val tclTHENFIRST : tactic -> tactic -> tactic
@@ -127,9 +128,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 +244,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..15c25b3467 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
@@ -180,7 +181,7 @@ let introduction ?(check=true) id =
let env = Proofview.Goal.env gl in
let () = if check && mem_named_context_val id hyps then
user_err ~hdr:"Tactics.introduction"
- (str "Variable " ++ pr_id id ++ str " is already declared.")
+ (str "Variable " ++ Id.print id ++ str " is already declared.")
in
let open Context.Named.Declaration in
match EConstr.kind sigma concl with
@@ -243,11 +244,11 @@ let convert_leq x y = convert_gen Reduction.CUMUL x y
let clear_dependency_msg env sigma id = function
| Evarutil.OccurHypInSimpleClause None ->
- pr_id id ++ str " is used in conclusion."
+ Id.print id ++ str " is used in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
- pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str"."
+ Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
- str "Cannot remove " ++ pr_id id ++
+ str "Cannot remove " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
@@ -256,12 +257,12 @@ let error_clear_dependency env sigma id err =
let replacing_dependency_msg env sigma id = function
| Evarutil.OccurHypInSimpleClause None ->
- str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion."
+ str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
- str "Cannot change " ++ pr_id id ++
- strbrk ", it is used in hypothesis " ++ pr_id id' ++ str"."
+ str "Cannot change " ++ Id.print id ++
+ strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
- str "Cannot change " ++ pr_id id ++
+ str "Cannot change " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
@@ -359,7 +360,7 @@ let rename_hyp repl =
let () =
try
let elt = Id.Set.choose (Id.Set.inter dst mods) in
- CErrors.user_err (pr_id elt ++ str " is already used")
+ CErrors.user_err (Id.print elt ++ str " is already used")
with Not_found -> ()
in
(** All is well *)
@@ -434,7 +435,7 @@ let find_name mayrepl decl naming gl = match naming with
let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in
let id' = next_ident_away id ids_of_hyps in
if not mayrepl && not (Id.equal id' id) then
- user_err ?loc (pr_id id ++ str" is already used.");
+ user_err ?loc (Id.print id ++ str" is already used.");
id
(**************************************************************)
@@ -488,7 +489,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
sign',t,concl,sigma
else
(if check && mem_named_context_val id sign then
- user_err (str "Variable " ++ pr_id id ++ str " is already declared.");
+ user_err (str "Variable " ++ Id.print id ++ str " is already declared.");
push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in
let nf_t = nf_betaiota sigma t in
Proofview.tclTHEN
@@ -580,11 +581,11 @@ 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"
- (str "Name " ++ pr_id f ++ str " already used in the environment");
+ (str "Name " ++ Id.print f ++ str " already used in the environment");
mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
in
let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
@@ -674,7 +675,7 @@ let pf_reduce_decl redfun where decl gl =
match decl with
| LocalAssum (id,ty) ->
if where == InHypValueOnly then
- user_err (pr_id id ++ str " has no value.");
+ user_err (Id.print id ++ str " has no value.");
LocalAssum (id,redfun' ty)
| LocalDef (id,b,ty) ->
let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -775,7 +776,7 @@ let pf_e_reduce_decl redfun where decl gl =
match decl with
| LocalAssum (id,ty) ->
if where == InHypValueOnly then
- user_err (pr_id id ++ str " has no value.");
+ user_err (Id.print id ++ str " has no value.");
let (sigma, ty') = redfun sigma ty in
(sigma, LocalAssum (id, ty'))
| LocalDef (id,b,ty) ->
@@ -818,7 +819,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
match decl with
| LocalAssum (id,ty) ->
if where == InHypValueOnly then
- user_err (pr_id id ++ str " has no value.");
+ user_err (Id.print id ++ str " has no value.");
let (sigma, ty') = redfun false env sigma ty in
(sigma, LocalAssum (id, ty'))
| LocalDef (id,b,ty) ->
@@ -1132,7 +1133,7 @@ let is_quantified_hypothesis id gl =
let msg_quantified_hypothesis = function
| NamedHyp id ->
- str "quantified hypothesis named " ++ pr_id id
+ str "quantified hypothesis named " ++ Id.print id
| AnonHyp n ->
pr_nth n ++
str " non dependent hypothesis"
@@ -1283,14 +1284,14 @@ let error_uninstantiated_metas t clenv =
let t = EConstr.Unsafe.to_constr t in
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.")
- in user_err (str "Cannot find an instance for " ++ pr_id id ++ str".")
+ in user_err (str "Cannot find an instance for " ++ Id.print id ++ str".")
let check_unresolved_evars_of_metas sigma clenv =
(* This checks that Metas turned into Evars by *)
(* 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
@@ -1475,7 +1476,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
let sort = Tacticals.New.elimination_sort_of_goal gl in
let mind = on_snd (fun u -> EInstance.kind sigma u) mind in
let (sigma, elim) =
- if occur_term sigma c concl then
+ if dependent sigma c concl then
build_case_analysis_scheme env sigma mind true sort
else
build_case_analysis_scheme_default env sigma mind sort in
@@ -1592,7 +1593,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
let new_hyp_typ = clenv_type elimclause'' in
if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
user_err ~hdr:"general_rewrite_in"
- (str "Nothing to rewrite in " ++ pr_id id ++ str".");
+ (str "Nothing to rewrite in " ++ Id.print id ++ str".");
clenv_refine_in with_evars id id sigma elimclause''
(fun id -> Proofview.tclUNIT ())
end
@@ -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 =
@@ -2045,8 +2046,8 @@ let assumption =
let on_the_bodies = function
| [] -> assert false
-| [id] -> str " depends on the body of " ++ pr_id id
-| l -> str " depends on the bodies of " ++ pr_sequence pr_id l
+| [id] -> str " depends on the body of " ++ Id.print id
+| l -> str " depends on the bodies of " ++ pr_sequence Id.print l
exception DependsOnBody of Id.t option
@@ -2083,7 +2084,7 @@ let clear_body ids =
let map = function
| LocalAssum (id,t) as decl ->
let () = if List.mem_f Id.equal id ids then
- user_err (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
+ user_err (str "Hypothesis " ++ Id.print id ++ str " is not a local definition")
in
decl
| LocalDef (id,_,t) as decl ->
@@ -2115,7 +2116,7 @@ let clear_body ids =
with DependsOnBody where ->
let msg = match where with
| None -> str "Conclusion" ++ on_the_bodies ids
- | Some id -> str "Hypothesis " ++ pr_id id ++ on_the_bodies ids
+ | Some id -> str "Hypothesis " ++ Id.print id ++ on_the_bodies ids
in
Tacticals.New.tclZEROMSG msg
in
@@ -2418,10 +2419,10 @@ let rec check_name_unicity env ok seen = function
| (loc, IntroNaming (IntroIdentifier id)) :: l ->
(try
ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env);
- user_err ?loc (pr_id id ++ str" is already used.")
+ user_err ?loc (Id.print id ++ str" is already used.")
with Not_found ->
if List.mem_f Id.equal id seen then
- user_err ?loc (pr_id id ++ str" is used twice.")
+ user_err ?loc (Id.print id ++ str" is used twice.")
else
check_name_unicity env ok (id::seen) l)
| (_, IntroAction (IntroOrAndPattern l)) :: l' ->
@@ -2742,7 +2743,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
| IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env
| IntroIdentifier id ->
if List.mem id (ids_of_named_context (named_context env)) then
- user_err ?loc (pr_id id ++ str" is already used.");
+ user_err ?loc (Id.print id ++ str" is already used.");
id in
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
@@ -2825,7 +2826,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
let generalized_name env sigma c t ids cl = function
| Name id as na ->
if Id.List.mem id ids then
- user_err (pr_id id ++ str " is already used.");
+ user_err (Id.print id ++ str " is already used.");
na
| Anonymous ->
match EConstr.kind sigma c with
@@ -3075,7 +3076,7 @@ let unfold_body x =
let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
let xval = match Environ.lookup_named x env with
| LocalAssum _ -> user_err ~hdr:"unfold_body"
- (pr_id x ++ str" is not a defined hypothesis.")
+ (Id.print x ++ str" is not a defined hypothesis.")
| LocalDef (_,xval,_) -> xval
in
let xval = EConstr.of_constr xval in
@@ -3912,7 +3913,7 @@ let specialize_eqs id =
(internal_cut true id ty')
(exact_no_check ((* refresh_universes_strict *) acc'))
else
- Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id)
+ Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ Id.print id)
end
let specialize_eqs id = Proofview.Goal.enter begin fun gl ->
@@ -4368,7 +4369,7 @@ let clear_unselected_context id inhyps cls =
if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) &&
cls.concl_occs == NoOccurrences
then user_err
- (str "Conclusion must be mentioned: it depends on " ++ pr_id id
+ (str "Conclusion must be mentioned: it depends on " ++ Id.print id
++ str ".");
match cls.onhyps with
| Some hyps ->
@@ -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-04-29 17:33:33 +0000