aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.mli2
-rw-r--r--proofs/evar_refiner.ml1
-rw-r--r--proofs/evar_refiner.mli1
-rw-r--r--proofs/goal.ml3
-rw-r--r--proofs/goal.mli3
-rw-r--r--proofs/logic.ml23
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/pfedit.ml28
-rw-r--r--proofs/pfedit.mli84
-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.mli15
16 files changed, 32 insertions, 142 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 9c69995f4b..9a2026dd37 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/evar_refiner.ml b/proofs/evar_refiner.ml
index 48fa2202ee..d38ff7512f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -14,6 +14,7 @@ open Evarutil
open Evarsolve
open Pp
open Glob_term
+open Ltac_pretype
(******************************************)
(* Instantiation of existential variables *)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 5d69715967..a0e3b718a2 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -8,6 +8,7 @@
open Evd
open Glob_term
+open Ltac_pretype
(** Refinement of existential variables. *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7d830146f9..19f816a019 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -21,7 +21,6 @@ type goal = Evd.evar
let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e)
let uid e = string_of_int (Evar.repr e)
-let get_by_uid u = Evar.unsafe_of_int (int_of_string u)
(* Layer to implement v8.2 tactic engine ontop of the new architecture.
Types are different from what they used to be due to a change of the
@@ -100,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/goal.mli b/proofs/goal.mli
index 6d3ec8bd4e..ad968cdfb3 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -15,9 +15,6 @@ type goal = Evar.t
(* Gives a unique identifier to each goal. The identifier is
guaranteed to contain no space. *)
val uid : goal -> string
-(* Returns the goal (even if it has been partially solved)
- corresponding to a unique identifier obtained by {!uid}. *)
-val get_by_uid : string -> goal
(* Debugging help *)
val pr_goal : goal -> Pp.t
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 20d075ae14..a633238f43 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 9d0756b332..7df7fd66bc 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.ml b/proofs/pfedit.ml
index 469e1a011e..2d4aba17cb 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -230,31 +230,3 @@ let apply_implicit_tactic tac = (); fun env sigma evk ->
let solve_by_implicit_tactic () = match !implicit_tactic with
| None -> None
| Some tac -> Some (apply_implicit_tactic tac)
-
-(** Deprecated functions *)
-let refining = Proof_global.there_are_pending_proofs
-let check_no_pending_proofs = Proof_global.check_no_pending_proof
-
-let get_current_proof_name = Proof_global.get_current_proof_name
-let get_all_proof_names = Proof_global.get_all_proof_names
-
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-
-let delete_proof = Proof_global.discard
-let delete_current_proof = Proof_global.discard_current
-let delete_all_proofs = Proof_global.discard_all
-
-let get_pftreestate () =
- Proof_global.give_me_the_proof ()
-
-let set_end_tac tac =
- Proof_global.set_endline_tactic tac
-
-let set_used_variables l =
- Proof_global.set_used_variables l
-
-let get_used_variables () =
- Proof_global.get_used_variables ()
-
-let get_universe_decl () =
- Proof_global.get_universe_decl ()
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6e4ecd13b3..21a65f8eb6 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -8,9 +8,8 @@
(** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
-open Loc
open Names
-open Term
+open Constr
open Environ
open Decl_kinds
@@ -122,84 +121,3 @@ val clear_implicit_tactic : unit -> unit
(* Raise Exit if cannot solve *)
val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
-
-(** {5 Deprecated functions in favor of [Proof_global]} *)
-
-(** {6 ... } *)
-(** Several proofs can be opened simultaneously but at most one is
- focused at some time. The following functions work by side-effect
- on current set of open proofs. In this module, ``proofs'' means an
- open proof (something started by vernacular command [Goal], [Lemma]
- or [Theorem]), and ``goal'' means a subgoal of the current focused
- proof *)
-
-(** [refining ()] tells if there is some proof in progress, even if a not
- focused one *)
-
-val refining : unit -> bool
-[@@ocaml.deprecated "use Proof_global.there_are_pending_proofs"]
-
-(** [check_no_pending_proofs ()] fails if there is still some proof in
- progress *)
-
-val check_no_pending_proofs : unit -> unit
-[@@ocaml.deprecated "use Proof_global.check_no_pending_proofs"]
-
-(** {6 ... } *)
-(** [delete_proof name] deletes proof of name [name] or fails if no proof
- has this name *)
-
-val delete_proof : Id.t located -> unit
-[@@ocaml.deprecated "use Proof_global.discard"]
-
-(** [delete_current_proof ()] deletes current focused proof or fails if
- no proof is focused *)
-
-val delete_current_proof : unit -> unit
-[@@ocaml.deprecated "use Proof_global.discard_current"]
-
-(** [delete_all_proofs ()] deletes all open proofs if any *)
-val delete_all_proofs : unit -> unit
-[@@ocaml.deprecated "use Proof_global.discard_all"]
-
-(** [get_pftreestate ()] returns the current focused pending proof.
- @raise NoCurrentProof if there is no pending proof. *)
-
-val get_pftreestate : unit -> Proof.proof
-[@@ocaml.deprecated "use Proof_global.give_me_the_proof"]
-
-(** {6 ... } *)
-(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
- by [solve] *)
-
-val set_end_tac : Genarg.glob_generic_argument -> unit
-[@@ocaml.deprecated "use Proof_global.set_endline_tactic"]
-
-(** {6 ... } *)
-(** [set_used_variables l] declares that section variables [l] will be
- used in the proof *)
-val set_used_variables :
- Id.t list -> Context.Named.t * Names.Id.t Loc.located list
-[@@ocaml.deprecated "use Proof_global.set_used_variables"]
-
-val get_used_variables : unit -> Context.Named.t option
-[@@ocaml.deprecated "use Proof_global.get_used_variables"]
-
-(** {6 Universe binders } *)
-val get_universe_decl : unit -> Univdecls.universe_decl
-[@@ocaml.deprecated "use Proof_global.get_universe_decl"]
-
-(** {6 ... } *)
-(** [get_current_proof_name ()] return the name of the current focused
- proof or failed if no proof is focused *)
-val get_current_proof_name : unit -> Id.t
-[@@ocaml.deprecated "use Proof_global.get_current_proof_name"]
-
-(** [get_all_proof_names ()] returns the list of all pending proof names.
- The first name is the current proof, the other names may come in
- any order. *)
-val get_all_proof_names : unit -> Id.t list
-[@@ocaml.deprecated "use Proof_global.get_all_proof_names"]
-
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-[@@ocaml.deprecated "use Proof_global.lemma_possible_guards"]
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 621178982d..97faa16848 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 8c0f6ad85f..6309f681f8 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 2ad5f607f2..20293cb9b3 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 ccc2440a2f..43e5987733 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 3b0a9e5b6f..cfdcde36e0 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 3ff010fe3e..9c8777c413 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 7e6d83b10f..6441cfd195 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
@@ -15,6 +15,7 @@ open Proof_type
open Redexpr
open Pattern
open Locus
+open Ltac_pretype
(** Operations for handling terms under a local typing context. *)
@@ -96,7 +97,7 @@ val pr_glls : goal list sigma -> Pp.t
(* Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
- val pf_global : identifier -> 'a Proofview.Goal.t -> Globnames.global_reference
+ val pf_global : Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference
(** FIXME: encapsulate the level in an existential type. *)
val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
@@ -117,13 +118,13 @@ module New : sig
val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types
val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool
- val pf_get_new_id : identifier -> 'a Proofview.Goal.t -> identifier
- val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
+ val pf_get_new_id : Id.t -> 'a Proofview.Goal.t -> Id.t
+ val pf_ids_of_hyps : 'a Proofview.Goal.t -> Id.t list
val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t
- val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
+ val pf_hyps_types : 'a Proofview.Goal.t -> (Id.t * types) list
- val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration
- val pf_get_hyp_typ : identifier -> 'a Proofview.Goal.t -> types
+ val pf_get_hyp : Id.t -> 'a Proofview.Goal.t -> named_declaration
+ val pf_get_hyp_typ : Id.t -> 'a Proofview.Goal.t -> types
val pf_last_hyp : 'a Proofview.Goal.t -> named_declaration
val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 00:28:09 +0000