diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 13 | ||||
| -rw-r--r-- | proofs/clenv.mli | 2 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 27 | ||||
| -rw-r--r-- | proofs/goal.ml | 3 | ||||
| -rw-r--r-- | proofs/proof.ml | 2 | ||||
| -rw-r--r-- | proofs/refine.ml | 2 |
6 files changed, 16 insertions, 33 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 7ebc789aa5..d25ae38c53 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 (******************************************************************) @@ -608,8 +608,7 @@ let make_evar_clause env sigma ?len t = else match EConstr.kind sigma t with | Cast (t, _, _) -> clrec (sigma, holes) n t | Prod (na, t1, t2) -> - let (sigma, ev) = new_evar env sigma t1 in - let sigma = Evd.set_resolvable_evar sigma (fst (destEvar sigma ev)) false in + let (sigma, ev) = new_evar env sigma ~typeclass_candidate:false 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 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 929443a969..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 ev evi = - let res = Evd.is_resolvable_evar evd ev 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 6aff43f741..4e540de538 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -64,8 +64,7 @@ module V82 = struct Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); Evd.evar_candidates = None } in - let (evars, evk) = Evarutil.new_pure_evar_full evars evi in - let evars = Evd.set_resolvable_evar evars evk false 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 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 |