aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml33
-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.ml10
-rw-r--r--proofs/proof.ml2
-rw-r--r--proofs/refine.ml2
-rw-r--r--proofs/tacmach.ml9
-rw-r--r--proofs/tacmach.mli3
10 files changed, 52 insertions, 67 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 95e908c4dd..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
(******************************************************************)
@@ -577,7 +577,7 @@ let pr_clenv clenv =
h 0
(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.evd)
+ 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 285240872e..4d5711c195 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -350,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
@@ -384,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
@@ -433,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;
@@ -447,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)
@@ -590,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/proof.ml b/proofs/proof.ml
index 70a08e4966..8220949856 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -386,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
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 05474d5f84..540a8bb420 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -105,7 +105,7 @@ 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()++
Termops.Internal.print_constr_env env sigma c)) in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5d1faf1465..231a8fe266 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -68,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,10 +130,10 @@ let db_pr_goal sigma g =
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 *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 3432ad4afa..14c83a6802 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -34,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
@@ -83,6 +83,7 @@ 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 *)
module New : sig
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 06:02:07 +0000