aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml37
-rw-r--r--proofs/clenv.mli2
-rw-r--r--proofs/clenvtac.ml27
-rw-r--r--proofs/goal.ml21
-rw-r--r--proofs/goal.mli10
-rw-r--r--proofs/logic.ml19
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/proof.ml7
-rw-r--r--proofs/proof.mli4
-rw-r--r--proofs/proof_bullet.ml3
-rw-r--r--proofs/proof_bullet.mli6
-rw-r--r--proofs/proof_global.ml5
-rw-r--r--proofs/proof_global.mli2
-rw-r--r--proofs/redexpr.ml9
-rw-r--r--proofs/refine.ml7
-rw-r--r--proofs/refine.mli4
-rw-r--r--proofs/refiner.mli8
-rw-r--r--proofs/tacmach.ml27
-rw-r--r--proofs/tacmach.mli18
19 files changed, 76 insertions, 142 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 79b7e1599b..b7ccd647b5 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -324,21 +324,21 @@ let adjust_meta_source evd mv = function
*)
let clenv_pose_metas_as_evars clenv dep_mvs =
- let rec fold clenv = function
- | [] -> clenv
+ let rec fold clenv evs = function
+ | [] -> clenv, evs
| mv::mvs ->
let ty = clenv_meta_type clenv mv in
(* Postpone the evar-ization if dependent on another meta *)
(* This assumes no cycle in the dependencies - is it correct ? *)
- if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
+ if occur_meta clenv.evd ty then fold clenv evs (mvs@[mv])
else
let src = evar_source_of_meta mv clenv.evd in
let src = adjust_meta_source clenv.evd mv src 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
+ fold clenv (fst (destEvar evd evar) :: evs) mvs in
+ fold clenv [] dep_mvs
(******************************************************************)
@@ -575,9 +575,9 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
let pr_clenv clenv =
h 0
- (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
- str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
- pr_evar_map (Some 2) clenv.evd)
+ (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++
+ str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++
+ pr_evar_map (Some 2) clenv.env clenv.evd)
(****************************************************************)
(** Evar version of mk_clenv *)
@@ -603,13 +603,20 @@ let make_evar_clause env sigma ?len t =
in
(** FIXME: do the renaming online *)
let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
- let rec clrec (sigma, holes) n t =
+ let rec clrec (sigma, holes) inst n t =
if n = 0 then (sigma, holes, t)
else match EConstr.kind sigma t with
- | Cast (t, _, _) -> clrec (sigma, holes) n t
+ | Cast (t, _, _) -> clrec (sigma, holes) inst n t
| Prod (na, t1, t2) ->
- let store = Typeclasses.set_resolvable Evd.Store.empty false in
- let (sigma, ev) = new_evar ~store env sigma t1 in
+ (** Share the evar instances as we are living in the same context *)
+ let inst, ctx, args, subst = match inst with
+ | None ->
+ (** Dummy type *)
+ let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in
+ Some (ctx, args, subst), ctx, args, subst
+ | Some (ctx, args, subst) -> inst, ctx, args, subst
+ in
+ let (sigma, ev) = new_evar_instance ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) args in
let dep = not (noccurn sigma 1 t2) in
let hole = {
hole_evar = ev;
@@ -619,11 +626,11 @@ let make_evar_clause env sigma ?len t =
hole_name = na;
} in
let t2 = if dep then subst1 ev t2 else t2 in
- clrec (sigma, hole :: holes) (pred n) t2
- | LetIn (na, b, _, t) -> clrec (sigma, holes) n (subst1 b t)
+ clrec (sigma, hole :: holes) inst (pred n) t2
+ | LetIn (na, b, _, t) -> clrec (sigma, holes) inst n (subst1 b t)
| _ -> (sigma, holes, t)
in
- let (sigma, holes, t) = clrec (sigma, []) bound t in
+ let (sigma, holes, t) = clrec (sigma, []) None bound t in
let holes = List.rev holes in
let clause = { cl_concl = t; cl_holes = holes } in
(sigma, clause)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f9506290a0..03acb9e46e 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -72,7 +72,7 @@ val clenv_unique_resolver :
val clenv_dependent : clausenv -> metavariable list
-val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * Evar.t list
(** {6 Bindings } *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ba4cde6d67..77f5804665 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -62,37 +62,19 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
(RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
clenv_pose_metas_as_evars clenv dep_mvs
-(** Use our own fast path, more informative than from Typeclasses *)
-let check_tc evd =
- let has_resolvable = ref false in
- let check _ evi =
- let res = Typeclasses.is_resolvable evi in
- if res then
- let () = has_resolvable := true in
- Typeclasses.is_class_evar evd evi
- else false
- in
- let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
- (has_typeclass, !has_resolvable)
-
let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
(** ppedrot: a Goal.enter here breaks things, because the tactic below may
solve goals by side effects, while the compatibility layer keeps those
useless goals. That deserves a FIXME. *)
Proofview.V82.tactic begin fun gl ->
- let clenv = clenv_pose_dependent_evars ~with_evars clenv in
+ let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
let evd' =
if with_classes then
- let (has_typeclass, has_resolvable) = check_tc clenv.evd in
let evd' =
- if has_typeclass then
- Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars
+ Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
~fail:(not with_evars) ~split:false clenv.env clenv.evd
- else clenv.evd
in
- if has_resolvable then
- Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
- else evd'
+ Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd'
else clenv.evd
in
let clenv = { clenv with evd = evd' } in
@@ -101,6 +83,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
(refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
end
+let clenv_pose_dependent_evars ?(with_evars=false) clenv =
+ fst (clenv_pose_dependent_evars ~with_evars clenv)
+
open Unification
let dft = default_unify_flags
diff --git a/proofs/goal.ml b/proofs/goal.ml
index c14c0a8a77..7245d4a004 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -50,13 +50,8 @@ module V82 = struct
let evi = Evd.find evars gl in
evi.Evd.evar_concl
- (* Access to ".evar_extra" *)
- let extra evars gl =
- let evi = Evd.find evars gl in
- evi.Evd.evar_extra
-
(* Old style mk_goal primitive *)
- let mk_goal evars hyps concl extra =
+ let mk_goal evars hyps concl =
(* A goal created that way will not be used by refine and will not
be shelved. It must not appear as a future_goal, so the future
goals are restored to their initial value after the evar is
@@ -67,11 +62,9 @@ module V82 = struct
Evd.evar_filter = Evd.Filter.identity;
Evd.evar_body = Evd.Evar_empty;
Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
- Evd.evar_candidates = None;
- Evd.evar_extra = extra }
+ Evd.evar_candidates = None }
in
- let evi = Typeclasses.mark_unresolvable evi in
- let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
+ let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
let evars = Evd.restore_future_goals evars prev_future_goals in
let ctxt = Environ.named_context_of_val hyps in
let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
@@ -79,18 +72,18 @@ module V82 = struct
(evk, ev, evars)
(* Instantiates a goal with an open term *)
- let partial_solution sigma evk c =
+ let partial_solution env sigma evk c =
(* Check that the goal itself does not appear in the refined term *)
let _ =
if not (Evarutil.occur_evar_upto sigma evk c) then ()
- else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
+ else Pretype_errors.error_occur_check env sigma evk c
in
Evd.define evk c sigma
(* Instantiates a goal with an open term, using name of goal for evk' *)
- let partial_solution_to sigma evk evk' c =
+ let partial_solution_to env sigma evk evk' c =
let id = Evd.evar_ident evk sigma in
- let sigma = partial_solution sigma evk c in
+ let sigma = partial_solution env sigma evk c in
match id with
| None -> sigma
| Some id -> Evd.rename evk' id sigma
diff --git a/proofs/goal.mli b/proofs/goal.mli
index a033d6daab..af9fb662bf 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -39,24 +39,20 @@ module V82 : sig
(* Access to ".evar_concl" *)
val concl : Evd.evar_map -> goal -> EConstr.constr
- (* Access to ".evar_extra" *)
- val extra : Evd.evar_map -> goal -> Evd.Store.t
-
- (* Old style mk_goal primitive, returns a new goal with corresponding
+ (* Old style mk_goal primitive, returns a new goal with corresponding
hypotheses and conclusion, together with a term which is precisely
the evar corresponding to the goal, and an updated evar_map. *)
val mk_goal : Evd.evar_map ->
Environ.named_context_val ->
EConstr.constr ->
- Evd.Store.t ->
goal * EConstr.constr * Evd.evar_map
(* Instantiates a goal with an open term *)
- val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
+ val partial_solution : Environ.env -> Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
(* Instantiates a goal with an open term, reusing name of goal for
second goal *)
- val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
+ val partial_solution_to : Environ.env -> Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
(* Principal part of the progress tactical *)
val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 613581ade7..4d5711c195 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -230,8 +230,7 @@ let hyp_of_move_location = function
| MoveBefore id -> id
| _ -> assert false
-let move_hyp sigma toleft (left,declfrom,right) hto =
- let env = Global.env() in
+let move_hyp env sigma toleft (left,declfrom,right) hto =
let test_dep d d2 =
if toleft
then occur_var_in_decl env sigma (NamedDecl.get_id d2) d
@@ -280,11 +279,11 @@ let move_hyp_in_named_context env sigma hfrom hto sign =
let open EConstr in
let (left,right,declfrom,toleft) =
split_sign env sigma hfrom hto (named_context_of_val sign) in
- move_hyp sigma toleft (left,declfrom,right) hto
+ move_hyp env sigma toleft (left,declfrom,right) hto
-let insert_decl_in_named_context sigma decl hto sign =
+let insert_decl_in_named_context env sigma decl hto sign =
let open EConstr in
- move_hyp sigma false ([],decl,named_context_of_val sign) hto
+ move_hyp env sigma false ([],decl,named_context_of_val sign) hto
(**********************************************************************)
@@ -351,7 +350,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
let env = Goal.V82.env sigma goal in
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)
+ Goal.V82.mk_goal sigma hyps concl
in
if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in
@@ -385,7 +384,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| App (f,l) ->
let (acc',hdty,sigma,applicand) =
- if is_template_polymorphic env sigma (EConstr.of_constr f) then
+ if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then
let ty =
(* Template polymorphism of definitions and inductive types *)
let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
@@ -434,7 +433,7 @@ and mk_hdgoals sigma goal goalacc trm =
let env = Goal.V82.env sigma goal in
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
+ Goal.V82.mk_goal sigma hyps concl in
match kind trm with
| Cast (c,_, ty) when isMeta c ->
check_typability env sigma ty;
@@ -448,7 +447,7 @@ and mk_hdgoals sigma goal goalacc trm =
| App (f,l) ->
let (acc',hdty,sigma,applicand) =
- if is_template_polymorphic env sigma (EConstr.of_constr f)
+ if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f)
then
let l' = meta_free_prefix sigma l in
(goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
@@ -591,5 +590,5 @@ let prim_refiner r sigma goal =
check_meta_variables env sigma c;
let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
let sgl = List.rev sgl in
- let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in
+ let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
(sgl, sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 9db54732bb..2cad278e10 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -75,6 +75,6 @@ val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location ->
Environ.named_context_val -> Environ.named_context_val
-val insert_decl_in_named_context : Evd.evar_map ->
+val insert_decl_in_named_context : Environ.env -> Evd.evar_map ->
EConstr.named_declaration -> Id.t move_location ->
Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8bbd82bb0a..8220949856 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -122,8 +122,6 @@ type t = {
initial_euctx : UState.t
}
-type proof = t
-
(*** General proof functions ***)
let proof p =
@@ -388,7 +386,7 @@ let run_tactic env tac pr =
(* Check that retrieved given up is empty *)
if not (List.is_empty retrieved_given_up) then
CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up.");
- let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in
+ let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
Proofview.tclUNIT retrieved
in
@@ -435,9 +433,6 @@ let pr_proof p =
(*** Compatibility layer with <=v8.2 ***)
module V82 = struct
- let subgoals p =
- let it, sigma = Proofview.proofview p.proofview in
- Evd.{ it; sigma }
let background_subgoals p =
let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 511dcc2e00..8cf543557b 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -33,8 +33,6 @@
(* Type of a proof. *)
type t
-type proof = t
-[@@ocaml.deprecated "please use [Proof.t]"]
(* Returns a stylised view of a proof for use by, for instance,
ide-s. *)
@@ -192,8 +190,6 @@ val pr_proof : t -> Pp.t
(*** Compatibility layer with <=v8.2 ***)
module V82 : sig
- val subgoals : t -> Goal.goal list Evd.sigma
- [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
(* All the subgoals of the proof, including those which are not focused. *)
val background_subgoals : t -> Goal.goal list Evd.sigma
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index cc3e79f858..ed8df29d7b 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -197,6 +197,3 @@ let put p b =
let suggest p =
(!current_behavior).suggest p
-
-let pr_goal_selector = Goal_select.pr_goal_selector
-let get_default_goal_selector = Goal_select.get_default_goal_selector
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index a09a7ec1d2..0fcc647a6f 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -44,9 +44,3 @@ val register_behavior : behavior -> unit
*)
val put : Proof.t -> t -> Proof.t
val suggest : Proof.t -> Pp.t
-
-(** Deprecated *)
-val pr_goal_selector : Goal_select.t -> Pp.t
-[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"]
-val get_default_goal_selector : unit -> Goal_select.t
-[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"]
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7e250faa86..25cf789193 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -101,7 +101,6 @@ type pstate = {
}
type t = pstate list
-type state = t
let make_terminator f = f
let apply_terminator f = f
@@ -348,8 +347,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
not (Safe_typing.empty_private_constants = eff))
in
let typ = if allow_deferred then t else nf t in
- let used_univs_body = Univops.universes_of_constr body in
- let used_univs_typ = Univops.universes_of_constr typ in
+ let used_univs_body = Vars.universes_of_constr body in
+ let used_univs_typ = Vars.universes_of_constr typ in
if allow_deferred then
let initunivs = UState.const_univ_entry ~poly initial_euctx in
let ctx = constrain_variables universes in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 854ceaa41a..2b04bfab57 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -13,8 +13,6 @@
environment. *)
type t
-type state = t
-[@@ocaml.deprecated "please use [Proof_global.t]"]
val there_are_pending_proofs : unit -> bool
val check_no_pending_proof : unit -> unit
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 44685d2bbd..56ce744bc1 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -15,7 +15,6 @@ open Names
open Constr
open EConstr
open Declarations
-open Globnames
open Genredexpr
open Pattern
open Reductionops
@@ -79,7 +78,7 @@ let set_strategy_one ref l =
| OpaqueDef _ ->
user_err ~hdr:"set_transparent_const"
(str "Cannot make" ++ spc () ++
- Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++
+ Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++
spc () ++ str "transparent because it was declared opaque.");
| _ -> Csymtable.set_transparent_const sp)
| _ -> ()
@@ -114,10 +113,8 @@ let classify_strategy (local,_ as obj) =
let disch_ref ref =
match ref with
- EvalConstRef c ->
- let c' = Lib.discharge_con c in
- if c==c' then Some ref else Some (EvalConstRef c')
- | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else Some ref
+ EvalConstRef c -> Some ref
+ | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref
let discharge_strategy (_,(local,obj)) =
if local then None else
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 198e057ebc..540a8bb420 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -44,9 +44,6 @@ let typecheck_evar ev env sigma =
let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
sigma
-let (pr_constrv,pr_constr) =
- Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
-
(* Get the side-effect's constant declarations to update the monad's
* environmnent *)
let add_if_undefined env eff =
@@ -108,10 +105,10 @@ let generic_refine ~typecheck f gl =
| Some id -> Evd.rename evk id sigma
in
(** Mark goals *)
- let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
+ let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
let trace () = Pp.(hov 2 (str"simple refine"++spc()++
- Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in
+ Termops.Internal.print_constr_env env sigma c)) in
Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
Proofview.Unsafe.tclEVARS sigma <*>
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 70a23a9fba..1af6463a02 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -17,10 +17,6 @@ open Proofview
(** {6 The refine tactic} *)
-(** Printer used to print the constr which refine refines. *)
-val pr_constr :
- (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t
-
(** {7 Refinement primitives} *)
val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 0f83e16ec8..30af6d8e1a 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -22,14 +22,6 @@ val project : 'a sigma -> evar_map
val pf_env : goal sigma -> Environ.env
val pf_hyps : goal sigma -> named_context
-val unpackage : 'a sigma -> evar_map ref * 'a
-[@@ocaml.deprecated "Do not use [evar_map ref]"]
-val repackage : evar_map ref -> 'a -> 'a sigma
-[@@ocaml.deprecated "Do not use [evar_map ref]"]
-val apply_sig_tac :
- evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
-[@@ocaml.deprecated "Do not use [evar_map ref]"]
-
val refiner : rule -> tactic
(** {6 Tacticals. } *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 092bb5c276..231a8fe266 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -30,14 +30,7 @@ let re_sig it gc = { it = it; sigma = gc; }
(* Operations for handling terms under a local typing context *)
(**************************************************************)
-type 'a sigma = 'a Evd.sigma;;
-type tactic = Proof_type.tactic;;
-
-[@@@ocaml.warning "-3"]
-let unpackage = Refiner.unpackage
-let repackage = Refiner.repackage
-let apply_sig_tac = Refiner.apply_sig_tac
-[@@@ocaml.warning "+3"]
+type tactic = Proof_type.tactic
let sig_it = Refiner.sig_it
let project = Refiner.project
@@ -75,7 +68,10 @@ let pf_ids_set_of_hyps gls =
let pf_get_new_id id gls =
next_ident_away id (pf_ids_set_of_hyps gls)
-let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
+let pf_global gls id =
+ let env = pf_env gls in
+ let sigma = project gls in
+ Evd.fresh_global env sigma (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
@@ -127,17 +123,17 @@ open Pp
let db_pr_goal sigma g =
let env = Goal.V82.env sigma g in
- let penv = print_named_context env in
- let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in
+ let penv = Termops.Internal.print_named_context env in
+ let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in
str" " ++ hv 0 (penv ++ fnl () ++
str "============================" ++ fnl () ++
str" " ++ pc) ++ fnl ()
let pr_gls gls =
- hov 0 (pr_evar_map (Some 2) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
+ hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
let pr_glls glls =
- hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++
+ hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++
prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls))
(* Variants of [Tacmach] functions built with the new proof engine *)
@@ -227,4 +223,9 @@ module New = struct
let pf_nf_evar gl t = nf_evar (project gl) t
+ let pf_undefined_evars gl =
+ let sigma = Proofview.Goal.sigma gl in
+ let ev = Proofview.Goal.goal gl in
+ let evi = Evd.find sigma ev in
+ Evarutil.filtered_undefined_evars_of_evar_info sigma evi
end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 31496fb3d5..14c83a6802 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -18,9 +18,6 @@ open Locus
(** Operations for handling terms under a local typing context. *)
-type 'a sigma = 'a Evd.sigma
-[@@ocaml.deprecated "alias of Evd.sigma"]
-
open Evd
type tactic = Proof_type.tactic;;
@@ -29,14 +26,6 @@ val project : goal sigma -> evar_map
val re_sig : 'a -> evar_map -> 'a sigma
-val unpackage : 'a sigma -> evar_map ref * 'a
-[@@ocaml.deprecated "Do not use [evar_map ref]"]
-val repackage : evar_map ref -> 'a -> 'a sigma
-[@@ocaml.deprecated "Do not use [evar_map ref]"]
-val apply_sig_tac :
- evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list)
-[@@ocaml.deprecated "Do not use [evar_map ref]"]
-
val pf_concl : goal sigma -> types
val pf_env : goal sigma -> env
val pf_hyps : goal sigma -> named_context
@@ -45,7 +34,7 @@ val pf_hyps_types : goal sigma -> (Id.t * types) list
val pf_nth_hyp_id : goal sigma -> int -> Id.t
val pf_last_hyp : goal sigma -> named_declaration
val pf_ids_of_hyps : goal sigma -> Id.t list
-val pf_global : goal sigma -> Id.t -> constr
+val pf_global : goal sigma -> Id.t -> evar_map * constr
val pf_unsafe_type_of : goal sigma -> constr -> types
val pf_type_of : goal sigma -> constr -> evar_map * types
val pf_hnf_type_of : goal sigma -> constr -> types
@@ -94,8 +83,9 @@ val refine : constr -> tactic
(** {6 Pretty-printing functions (debug only). } *)
val pr_gls : goal sigma -> Pp.t
val pr_glls : goal list sigma -> Pp.t
+[@@ocaml.deprecated "Please move to \"new\" proof engine"]
-(* Variants of [Tacmach] functions built with the new proof engine *)
+(** Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t
@@ -139,4 +129,6 @@ module New : sig
val pf_nf_evar : Proofview.Goal.t -> constr -> constr
+ (** Gathers the undefined evars of the given goal. *)
+ val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 01:44:14 +0000