aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.mli2
-rw-r--r--proofs/goal.ml2
-rw-r--r--proofs/logic.ml23
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--proofs/proof_global.mli2
-rw-r--r--proofs/proof_type.ml2
-rw-r--r--proofs/redexpr.mli2
-rw-r--r--proofs/refine.mli2
-rw-r--r--proofs/refiner.mli2
-rw-r--r--proofs/tacmach.mli2
12 files changed, 23 insertions, 22 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 9c69995f4..9a2026dd3 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -11,7 +11,7 @@
evar-based clauses. *)
open Names
-open Term
+open Constr
open Environ
open Evd
open EConstr
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 61f3e4a02..19f816a01 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -99,7 +99,7 @@ module V82 = struct
let same_goal evars1 gl1 evars2 gl2 =
let evi1 = Evd.find evars1 gl1 in
let evi2 = Evd.find evars2 gl2 in
- Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
+ Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl &&
Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
let weak_progress glss gls =
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 20d075ae1..a633238f4 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -12,6 +12,7 @@ open Util
open Names
open Nameops
open Term
+open Constr
open Vars
open Termops
open Environ
@@ -284,12 +285,12 @@ let error_unsupported_deep_meta c =
strbrk "supported; try \"refine\" instead.")
let collect_meta_variables c =
- let rec collrec deep acc c = match kind_of_term c with
+ let rec collrec deep acc c = match kind c with
| Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
| Cast(c,_,_) -> collrec deep acc c
- | (App _| Case _) -> Term.fold_constr (collrec deep) acc c
+ | (App _| Case _) -> Constr.fold (collrec deep) acc c
| Proj (_, c) -> collrec deep acc c
- | _ -> Term.fold_constr (collrec true) acc c
+ | _ -> Constr.fold (collrec true) acc c
in
List.rev (collrec false [] c)
@@ -332,7 +333,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
(goalacc,t'ty,sigma,trm)
else
- match kind_of_term trm with
+ match kind trm with
| Meta _ ->
let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
if !check && occur_meta sigma conclty then
@@ -372,7 +373,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
in
let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
- let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+ let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
(acc'',conclty',sigma, ans)
| Proj (p,c) ->
@@ -394,7 +395,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let lf' = Array.rev_of_list rbranches in
let ans =
if p' == p && c' == c && Array.equal (==) lf' lf then trm
- else Term.mkCase (ci,p',c',lf')
+ else mkCase (ci,p',c',lf')
in
(acc'',conclty',sigma, ans)
@@ -413,7 +414,7 @@ and mk_hdgoals sigma goal goalacc trm =
let hyps = Goal.V82.hyps sigma goal in
let mk_goal hyps concl =
Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
- match kind_of_term trm with
+ match kind trm with
| Cast (c,_, ty) when isMeta c ->
check_typability env sigma ty;
let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
@@ -433,7 +434,7 @@ and mk_hdgoals sigma goal goalacc trm =
else mk_hdgoals sigma goal goalacc f
in
let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
- let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in
+ let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
(acc'',conclty',sigma, ans)
| Case (ci,p,c,lf) ->
@@ -447,7 +448,7 @@ and mk_hdgoals sigma goal goalacc trm =
let lf' = Array.rev_of_list rbranches in
let ans =
if p' == p && c' == c && Array.equal (==) lf' lf then trm
- else Term.mkCase (ci,p',c',lf')
+ else mkCase (ci,p',c',lf')
in
(acc'',conclty',sigma, ans)
@@ -468,12 +469,12 @@ and mk_arggoals sigma goal goalacc funty allargs =
let foldmap (goalacc, funty, sigma) harg =
let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
let t = EConstr.Unsafe.to_constr t in
- let rec collapse t = match kind_of_term t with
+ let rec collapse t = match kind t with
| LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
| _ -> t
in
let t = collapse t in
- match kind_of_term t with
+ match kind t with
| Prod (_, c1, b) ->
let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in
(acc, subst1 harg b, sigma), arg
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 9d0756b33..7df7fd66b 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -9,7 +9,7 @@
(** Legacy proof engine. Do not use in newly written code. *)
open Names
-open Term
+open Constr
open Evd
open Proof_type
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6e4ecd13b..ec176e547 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -10,7 +10,7 @@
open Loc
open Names
-open Term
+open Constr
open Environ
open Decl_kinds
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 621178982..97faa1684 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -320,7 +320,7 @@ let constrain_variables init uctx =
let levels = Univ.Instance.levels (Univ.UContext.instance init) in
UState.constrain_variables levels uctx
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context
let close_proof ~keep_body_ucst_separate ?feedback_id ~now
(fpl : closed_proof_output Future.computation) =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 8c0f6ad85..6309f681f 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -86,7 +86,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
* Both access the current proof state. The former is supposed to be
* chained with a computation that completed the proof *)
-type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
+type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context
(* If allow_partial is set (default no) then an incomplete proof
* is allowed (no error), and a warn is given if the proof is complete. *)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 2ad5f607f..20293cb9b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -9,7 +9,7 @@
(** Legacy proof engine. Do not use in newly written code. *)
open Evd
-open Term
+open Constr
(** This module defines the structure of proof tree and the tactic type. So, it
is used by [Proof_tree] and [Refiner] *)
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index ccc2440a2..43e598773 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -9,7 +9,7 @@
(** Interpretation layer of redexprs such as hnf, cbv, etc. *)
open Names
-open Term
+open Constr
open EConstr
open Pattern
open Genredexpr
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 3b0a9e5b6..cfdcde36e 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -17,7 +17,7 @@ open Proofview
(** Printer used to print the constr which refine refines. *)
val pr_constr :
- (Environ.env -> Evd.evar_map -> Term.constr -> Pp.t) Hook.t
+ (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t
(** {7 Refinement primitives} *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 3ff010fe3..9c8777c41 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -37,7 +37,7 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic
val tclEVARS : evar_map -> tactic
val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
-val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic
+val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic
val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic
val tclPUSHCONSTRAINTS : Univ.constraints -> tactic
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index de9f8e700..6441cfd19 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Environ
open EConstr
open Evd
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 00:11:29 +0000