aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml14
-rw-r--r--proofs/clenv.mli8
-rw-r--r--proofs/clenvtac.ml9
-rw-r--r--proofs/goal.ml9
-rw-r--r--proofs/logic.ml6
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--proofs/proof_global.mli77
-rw-r--r--proofs/redexpr.ml4
-rw-r--r--proofs/refine.ml26
-rw-r--r--proofs/refine.mli8
-rw-r--r--proofs/refiner.ml6
-rw-r--r--proofs/tacmach.ml15
-rw-r--r--proofs/tacmach.mli48
14 files changed, 113 insertions, 121 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 33a86402ef..79d2e46942 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -25,7 +25,6 @@ open Pretype_errors
open Evarutil
open Unification
open Misctypes
-open Sigma.Notations
(******************************************************************)
(* Clausal environments *)
@@ -157,7 +156,7 @@ let error_incompatible_inst clenv mv =
(str "An incompatible instantiation has already been found for " ++
pr_id id)
| _ ->
- anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned")
+ anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.")
(* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)
let clenv_assign mv rhs clenv =
@@ -337,9 +336,8 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
else
let src = evar_source_of_meta mv clenv.evd in
let src = adjust_meta_source clenv.evd mv src in
- let evd = Sigma.Unsafe.of_evar_map clenv.evd in
- let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
- let evd = Sigma.to_evar_map evd in
+ let evd = clenv.evd in
+ let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
let clenv = clenv_assign mv evar {clenv with evd=evd} in
fold clenv mvs in
fold clenv dep_mvs
@@ -433,7 +431,7 @@ let explain_no_such_bound_variable evd id =
| Cltyp (na, _) -> na
| Clval (na, _, _) -> na
in
- if na != Anonymous then out_name na :: l else l
+ if na != Anonymous then Name.get_id na :: l else l
in
let mvl = List.fold_left fold [] (Evd.meta_list evd) in
user_err ~hdr:"Evd.meta_with_name"
@@ -614,9 +612,7 @@ let make_evar_clause env sigma ?len t =
| Cast (t, _, _) -> clrec (sigma, holes) n t
| Prod (na, t1, t2) ->
let store = Typeclasses.set_resolvable Evd.Store.empty false in
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
- let sigma = Sigma.to_evar_map sigma in
+ let (sigma, ev) = new_evar ~store env sigma t1 in
let dep = not (noccurn sigma 1 t2) in
let hole = {
hole_evar = ev;
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 4bcd50591c..f43c0531d4 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -41,10 +41,10 @@ val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr
(** type of a meta in clenv context *)
val clenv_meta_type : clausenv -> metavariable -> types
-val mk_clenv_from : ('a, 'r) Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_from : 'a Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
val mk_clenv_from_n :
- ('a, 'r) Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
-val mk_clenv_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> clausenv
+ 'a Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : 'a Proofview.Goal.t -> EConstr.constr -> clausenv
val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
(** Refresh the universes in a clenv *)
@@ -66,7 +66,7 @@ val old_clenv_unique_resolver :
?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
val clenv_unique_resolver :
- ?flags:unify_flags -> clausenv -> ('a, 'r) Proofview.Goal.t -> clausenv
+ ?flags:unify_flags -> clausenv -> 'a Proofview.Goal.t -> clausenv
val clenv_dependent : clausenv -> metavariable list
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 0722ea0470..2ce144a6d7 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -17,7 +17,6 @@ open Logic
open Reduction
open Tacmach
open Clenv
-open Proofview.Notations
(* This function put casts around metavariables whose type could not be
* infered by the refiner, that is head of applications, predicates and
@@ -104,10 +103,10 @@ open Unification
let dft = default_unify_flags
let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let clenv = clenv_unique_resolver ~flags clenv gl in
clenv_refine with_evars ~with_classes clenv
- end }
+ end
(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
particulier ne semblent pas vérifier que des instances différentes
@@ -139,7 +138,7 @@ let fail_quick_unif_flags = {
(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
let unify ?(flags=fail_quick_unif_flags) m =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Tacmach.New.pf_env gl in
let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
let evd = clear_metas (Tacmach.New.project gl) in
@@ -147,4 +146,4 @@ let unify ?(flags=fail_quick_unif_flags) m =
let evd' = w_unify env evd CONV ~flags m n in
Proofview.Unsafe.tclEVARSADVANCE evd'
with e when CErrors.noncritical e -> Proofview.tclZERO e
- end }
+ end
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 5a717f1662..e69ef18fd0 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -8,7 +8,6 @@
open Util
open Pp
-open Sigma.Notations
module NamedDecl = Context.Named.Declaration
@@ -73,9 +72,7 @@ module V82 = struct
Evd.evar_extra = extra }
in
let evi = Typeclasses.mark_unresolvable evi in
- let evars = Sigma.Unsafe.of_evar_map evars in
- let Sigma (evk, evars, _) = Evarutil.new_pure_evar_full evars evi in
- let evars = Sigma.to_evar_map evars in
+ let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
let ctxt = Environ.named_context_of_val hyps in
let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
@@ -131,9 +128,7 @@ module V82 = struct
let new_evi =
{ evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
let new_evi = Typeclasses.mark_unresolvable new_evi in
- let sigma = Sigma.Unsafe.of_evar_map Evd.empty in
- let Sigma (evk, sigma, _) = Evarutil.new_pure_evar_full sigma new_evi in
- let sigma = Sigma.to_evar_map sigma in
+ let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
{ Evd.it = evk ; sigma = sigma; }
(* Used by the compatibility layer and typeclasses *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index cd2cfbd32f..c329bdf4aa 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -414,7 +414,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| _ ->
if occur_meta sigma (EConstr.of_constr trm) then
- anomaly (Pp.str "refiner called with a meta in non app/case subterm");
+ anomaly (Pp.str "refiner called with a meta in non app/case subterm.");
let (sigma, t'ty) = goal_type_of env sigma trm in
let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
(goalacc,t'ty,sigma, trm)
@@ -474,7 +474,7 @@ and mk_hdgoals sigma goal goalacc trm =
| _ ->
if !check && occur_meta sigma (EConstr.of_constr trm) then
- anomaly (Pp.str "refine called with a dependent meta");
+ anomaly (Pp.str "refine called with a dependent meta.");
let (sigma, ty) = goal_type_of env sigma trm in
goalacc, ty, sigma, trm
@@ -502,7 +502,7 @@ and mk_casegoals sigma goal goalacc p c =
let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
let ((ind, u), spec) =
try Tacred.find_hnf_rectype env sigma ct
- with Not_found -> anomaly (Pp.str "mk_casegoals") in
+ with Not_found -> anomaly (Pp.str "mk_casegoals.") in
let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in
let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
(acc'',lbrty,conclty,sigma,p',c')
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index aaceb7b762..3fb66d1b87 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -113,7 +113,7 @@ let get_current_context () =
let current_proof_statement () =
match Proof_global.V82.get_current_initial_conclusions () with
| (id,([concl],strength)) -> id,strength,concl
- | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
+ | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.")
let solve ?with_end_tac gi info_lvl tac pr =
try
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4d2f534a76..5ec34a6387 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -719,7 +719,7 @@ type state = pstate list
let freeze ~marshallable =
match marshallable with
| `Yes ->
- CErrors.anomaly (Pp.str"full marshalling of proof state not supported")
+ CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
| `Shallow -> !pstates
| `No -> !pstates
let unfreeze s = pstates := s; update_proof_mode ()
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 52bbd9ac56..22cc8cf599 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -10,26 +10,6 @@
toplevel. In particular it defines the global proof
environment. *)
-(** Type of proof modes :
- - A name
- - A function [set] to set it *from standard mode*
- - A function [reset] to reset the *standard mode* from it
-
-*)
-type proof_mode_name = string
-type proof_mode = {
- name : proof_mode_name ;
- set : unit -> unit ;
- reset : unit -> unit
-}
-
-(** Registers a new proof mode which can then be adressed by name
- in [set_default_proof_mode].
- One mode is already registered - the standard mode - named "No",
- It corresponds to Coq default setting are they are set when coqtop starts. *)
-val register_proof_mode : proof_mode -> unit
-val get_default_proof_mode_name : unit -> proof_mode_name
-
val there_are_pending_proofs : unit -> bool
val check_no_pending_proof : unit -> unit
@@ -40,10 +20,6 @@ val discard : Names.Id.t Loc.located -> unit
val discard_current : unit -> unit
val discard_all : unit -> unit
-(** [set_proof_mode] sets the proof mode to be used after it's called. It is
- typically called by the Proof Mode command. *)
-val set_proof_mode : proof_mode_name -> unit
-
exception NoCurrentProof
val give_me_the_proof : unit -> Proof.proof
(** @raise NoCurrentProof when outside proof mode. *)
@@ -147,16 +123,6 @@ val get_universe_binders : unit -> universe_binders option
(**********************************************************)
(* *)
-(* Proof modes *)
-(* *)
-(**********************************************************)
-
-
-val activate_proof_mode : proof_mode_name -> unit
-val disactivate_current_proof_mode : unit -> unit
-
-(**********************************************************)
-(* *)
(* Bullets *)
(* *)
(**********************************************************)
@@ -211,3 +177,46 @@ val freeze : marshallable:[`Yes | `No | `Shallow] -> state
val unfreeze : state -> unit
val proof_of_state : state -> Proof.proof
val copy_terminators : src:state -> tgt:state -> state
+
+
+(**********************************************************)
+(* Proof Mode API *)
+(* The current Proof Mode API is deprecated and a new one *)
+(* will be (hopefully) defined in 8.8 *)
+(**********************************************************)
+
+(** Type of proof modes :
+ - A name
+ - A function [set] to set it *from standard mode*
+ - A function [reset] to reset the *standard mode* from it
+
+*)
+type proof_mode_name = string
+type proof_mode = {
+ name : proof_mode_name ;
+ set : unit -> unit ;
+ reset : unit -> unit
+}
+
+(** Registers a new proof mode which can then be adressed by name
+ in [set_default_proof_mode].
+ One mode is already registered - the standard mode - named "No",
+ It corresponds to Coq default setting are they are set when coqtop starts. *)
+val register_proof_mode : proof_mode -> unit
+(* Can't make this deprecated due to limitations of camlp5 *)
+(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *)
+
+val get_default_proof_mode_name : unit -> proof_mode_name
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
+(** [set_proof_mode] sets the proof mode to be used after it's called. It is
+ typically called by the Proof Mode command. *)
+val set_proof_mode : proof_mode_name -> unit
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
+val activate_proof_mode : proof_mode_name -> unit
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
+val disactivate_current_proof_mode : unit -> unit
+[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
+
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 7cd526843a..458dd21613 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -195,13 +195,13 @@ let decl_red_expr s e =
end
let out_arg = function
- | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
+ | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
| ArgArg x -> x
let out_with_occurrences (occs,c) =
(Locusops.occurrences_map (List.map out_arg) occs, c)
-let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm }
+let e_red f env evm c = evm, f env evm c
let head_style = false (* Turn to true to have a semantics where simpl
only reduce at the head when an evaluable reference is given, e.g.
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 63ae41075c..caa6b9fb30 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Util
-open Sigma.Notations
open Proofview.Notations
open Context.Named.Declaration
@@ -73,7 +72,6 @@ let add_side_effects env effects =
let generic_refine ?(unsafe = true) f gl =
let gl = Proofview.Goal.assume gl in
let sigma = Proofview.Goal.sigma gl in
- let sigma = Sigma.to_evar_map sigma in
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
(** Save the [future_goals] state to restore them after the
@@ -129,19 +127,20 @@ let generic_refine ?(unsafe = true) f gl =
let lift c =
Proofview.tclEVARMAP >>= fun sigma ->
Proofview.V82.wrap_exceptions begin fun () ->
- let Sigma (c, sigma, _) = c.run (Sigma.Unsafe.of_evar_map sigma) in
- Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () ->
+ let (sigma, c) = c sigma in
+ Proofview.Unsafe.tclEVARS sigma >>= fun () ->
Proofview.tclUNIT c
end
-let make_refine_enter ?unsafe f =
- { enter = fun gl -> generic_refine ?unsafe (lift f) gl }
+let make_refine_enter ?unsafe f gl = generic_refine ?unsafe (lift f) gl
let refine_one ?(unsafe = true) f =
Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
let refine ?(unsafe = true) f =
- let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in
+ let f evd =
+ let (evd,c) = f evd in (evd,((), c))
+ in
Proofview.Goal.enter (make_refine_enter ~unsafe f)
(** Useful definitions *)
@@ -154,17 +153,16 @@ let with_type env evd c t =
in
evd , j'.Environ.uj_val
-let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
+let refine_casted ?unsafe f = Proofview.Goal.enter begin fun gl ->
let gl = Proofview.Goal.assume gl in
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
- let f = { run = fun h ->
- let Sigma (c, h, p) = f.run h in
- let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
- Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
- } in
+ let f h =
+ let (h, c) = f h in
+ with_type env h c concl
+ in
refine ?unsafe f
-end }
+end
(** {7 solve_constraints}
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 5098f246a0..f1439f9a13 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -21,7 +21,7 @@ val pr_constr :
(** {7 Refinement primitives} *)
-val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
+val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
(** In [refine ?unsafe t], [t] is a term with holes under some
[evar_map] context. The term [t] is used as a partial solution
for the current goal (refine is a goal-dependent tactic), the
@@ -30,11 +30,11 @@ val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
tactic failures. If [unsafe] is [false] (default is [true]) [t] is
type-checked beforehand. *)
-val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
+val refine_one : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
(** A variant of [refine] which assumes exactly one goal under focus *)
val generic_refine : ?unsafe:bool -> ('a * EConstr.t) tactic ->
- ([ `NF ], 'r) Proofview.Goal.t -> 'a tactic
+ [ `NF ] Proofview.Goal.t -> 'a tactic
(** The general version of refine. *)
(** {7 Helper functions} *)
@@ -44,7 +44,7 @@ val with_type : Environ.env -> Evd.evar_map ->
(** [with_type env sigma c t] ensures that [c] is of type [t]
inserting a coercion if needed. *)
-val refine_casted : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
+val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
(** Like {!refine} except the refined term is coerced to the conclusion of the
current goal. *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 259e96a276..91e6dc4ab2 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -188,8 +188,6 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
(fun hypl -> List.subtract cmp hypl oldhyps)
hyps
in
- let emacs_str s =
- if !Flags.print_emacs then s else "" in
let s =
let frst = ref true in
List.fold_left
@@ -199,9 +197,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
"" lh))
"" newhyps in
Feedback.msg_notice
- (str (emacs_str "<infoH>")
+ (str "<infoH>"
++ (hov 0 (str s))
- ++ (str (emacs_str "</infoH>")));
+ ++ (str "</infoH>"));
tclIDTAC goal;;
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 97c5cda770..f9d9f25ccf 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -18,7 +18,6 @@ open Tacred
open Proof_type
open Logic
open Refiner
-open Sigma.Notations
open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
@@ -75,13 +74,12 @@ let pf_get_new_ids ids gls =
(fun id acc -> (next_ident_away id (acc@avoid))::acc)
ids []
-let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id)
+let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
let pf_reduction_of_red_expr gls re c =
let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
- let sigma = Sigma.Unsafe.of_evar_map (project gls) in
- let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in
- (Sigma.to_evar_map sigma, c)
+ let sigma = project gls in
+ redfun (pf_env gls) sigma c
let pf_apply f gls = f (pf_env gls) (project gls)
let pf_eapply f gls x =
@@ -158,8 +156,7 @@ let pr_glls glls =
module New = struct
let project gl =
- let sigma = Proofview.Goal.sigma gl in
- Sigma.to_evar_map sigma
+ Proofview.Goal.sigma gl
let pf_apply f gl =
f (Proofview.Goal.env gl) (project gl)
@@ -171,7 +168,7 @@ module New = struct
(** We only check for the existence of an [id] in [hyps] *)
let gl = Proofview.Goal.assume gl in
let hyps = Proofview.Goal.hyps gl in
- EConstr.of_constr (Constrintern.construct_reference hyps id)
+ Constrintern.construct_reference hyps id
let pf_env = Proofview.Goal.env
let pf_concl = Proofview.Goal.concl
@@ -216,7 +213,7 @@ module New = struct
let hyps = Proofview.Goal.hyps gl in
List.hd hyps
- let pf_nf_concl (gl : ([ `LZ ], 'r) Proofview.Goal.t) =
+ let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) =
(** We normalize the conclusion just after *)
let gl = Proofview.Goal.assume gl in
let concl = Proofview.Goal.concl gl in
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e6e60e27f7..3d2fa72c17 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -99,47 +99,47 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds
(* Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
- val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a
- val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr
+ val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
+ val pf_global : identifier -> '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 ], 'r) Proofview.Goal.t -> 'a
+ val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
- val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
- val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
- val pf_concl : ('a, 'r) Proofview.Goal.t -> types
+ val project : 'a Proofview.Goal.t -> Evd.evar_map
+ val pf_env : 'a Proofview.Goal.t -> Environ.env
+ val pf_concl : 'a Proofview.Goal.t -> types
(** WRONG: To be avoided at all costs, it typechecks the term entirely but
forgets the universe constraints necessary to retypecheck it *)
- val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+ val pf_unsafe_type_of : 'a Proofview.Goal.t -> constr -> types
(** This function does no type inference and expects an already well-typed term.
It recomputes its type in the fastest way possible (no conversion is ever involved) *)
- val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+ val pf_get_type_of : 'a Proofview.Goal.t -> constr -> types
(** This function entirely type-checks the term and computes its type
and the implied universe constraints. *)
- val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types
- val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool
+ 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, 'r) Proofview.Goal.t -> identifier
- val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
- val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list
+ val pf_get_new_id : identifier -> 'a Proofview.Goal.t -> identifier
+ val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
+ val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
- val pf_get_hyp : identifier -> ('a, 'r) Proofview.Goal.t -> named_declaration
- val pf_get_hyp_typ : identifier -> ('a, 'r) Proofview.Goal.t -> types
- val pf_last_hyp : ('a, 'r) Proofview.Goal.t -> named_declaration
+ val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration
+ val pf_get_hyp_typ : identifier -> 'a Proofview.Goal.t -> types
+ val pf_last_hyp : 'a Proofview.Goal.t -> named_declaration
- val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
- val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> (inductive * EInstance.t) * types
+ val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
+ val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> (inductive * EInstance.t) * types
- val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
- val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+ val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types
+ val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
- val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
- val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
+ val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr
+ val pf_compute : 'a Proofview.Goal.t -> constr -> constr
- val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+ val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
- val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr
+ val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 08:10:33 +0000