diff options
| -rw-r--r-- | tactics/auto.ml | 9 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 40 | ||||
| -rw-r--r-- | tactics/eauto.ml | 9 | ||||
| -rw-r--r-- | tactics/hints.ml | 50 | ||||
| -rw-r--r-- | tactics/hints.mli | 3 |
5 files changed, 52 insertions, 59 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 1ba35e9113..0931c3e61e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -15,7 +15,6 @@ open Termops open Environ open Genredexpr open Tactics -open Clenv open Locus open Proofview.Notations open Hints @@ -78,10 +77,10 @@ let unify_resolve_gen = function let exact h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (exact_check c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, c = Hints.fresh_hint env sigma h in + Proofview.Unsafe.tclEVARS sigma <*> exact_check c end (* Util *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 64d62a89b0..c4ef32974c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -144,18 +144,11 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st = } let e_give_exact flags h = - let { hint_term = c; hint_uctx = ctx } = h in let open Tacmach.New in Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = project gl in - let c, sigma = - if h.hint_poly then - let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in - let evd = Evd.merge_context_set Evd.univ_flexible sigma ctx in - let c = Vars.subst_univs_level_constr subst c in - c, evd - else c, sigma - in + let sigma, c = Hints.fresh_hint env sigma h in let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in Proofview.Unsafe.tclEVARS sigma <*> Clenv.unify ~flags t1 <*> exact_no_check c @@ -179,28 +172,21 @@ let unify_resolve ~with_evars flags h diff = match diff with let unify_resolve_refine flags h diff = let len = match diff with None -> None | Some (diff, _) -> Some diff in Proofview.Goal.enter begin fun gls -> - let { hint_term = c; hint_type = t; hint_uctx = ctx } = h in let open Clenv in let env = Proofview.Goal.env gls in let concl = Proofview.Goal.concl gls in Refine.refine ~typecheck:false begin fun sigma -> - let sigma, term, ty = - if h.hint_poly then - let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in - let map c = Vars.subst_univs_level_constr subst c in - let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in - sigma, map c, map t - else - let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in - sigma, c, t - in - let sigma', cl = Clenv.make_evar_clause env sigma ?len ty in - let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in - let sigma' = - Evarconv.(unify_leq_delay - ~flags:(default_flags_of flags.core_unify_flags.modulo_delta) - env sigma' cl.cl_concl concl) - in (sigma', term) end + let sigma, term = Hints.fresh_hint env sigma h in + let ty = Retyping.get_type_of env sigma term in + let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in + let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in + let sigma = + Evarconv.(unify_leq_delay + ~flags:(default_flags_of flags.core_unify_flags.modulo_delta) + env sigma cl.cl_concl concl) + in + (sigma, term) + end end let unify_resolve_refine flags h diff = diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 1bdf36b56c..9a554b117e 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -19,7 +19,6 @@ open Tacticals open Tacmach open Evd open Tactics -open Clenv open Auto open Genredexpr open Tactypes @@ -84,10 +83,10 @@ let hintmap_of sigma secvars concl = let e_exact flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (e_give_exact c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, c = Hints.fresh_hint env sigma h in + Proofview.Unsafe.tclEVARS sigma <*> e_give_exact c end let rec e_trivial_fail_db db_list local_db = diff --git a/tactics/hints.ml b/tactics/hints.ml index 683691d5c4..e029e4628d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1595,34 +1595,44 @@ struct end let connect_hint_clenv h gl = - let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in + let { hint_uctx = ctx; hint_clnv = clenv } = h in (* [clenv] has been generated by a hint-making function, so the only relevant data in its evarmap is the set of metas. The [evar_reset_evd] function below just replaces the metas of sigma by those coming from the clenv. *) let sigma = Tacmach.New.project gl in let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in (* Still, we need to update the universes *) - let clenv, c = - if h.hint_poly then - (* Refresh the instance of the hint *) - let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in - let emap c = Vars.subst_univs_level_constr subst c in - let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - (* Only metas are mentioning the old universes. *) - let clenv = { - templval = Evd.map_fl emap clenv.templval; - templtyp = Evd.map_fl emap clenv.templtyp; - evd = Evd.map_metas emap evd; - env = Proofview.Goal.env gl; - } in - clenv, emap c - else - let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - { clenv with evd = evd ; env = Proofview.Goal.env gl }, c - in clenv, c + if h.hint_poly then + (* Refresh the instance of the hint *) + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in + let emap c = Vars.subst_univs_level_constr subst c in + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + (* Only metas are mentioning the old universes. *) + let clenv = { + templval = Evd.map_fl emap clenv.templval; + templtyp = Evd.map_fl emap clenv.templtyp; + evd = Evd.map_metas emap evd; + env = Proofview.Goal.env gl; + } in + clenv + else + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + { clenv with evd = evd ; env = Proofview.Goal.env gl } + +let fresh_hint env sigma h = + let { hint_term = c; hint_uctx = ctx } = h in + if h.hint_poly then + (* Refresh the instance of the hint *) + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in + let c = Vars.subst_univs_level_constr subst c in + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + sigma, c + else + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + sigma, c let hint_res_pf ?with_evars ?with_classes ?flags h = Proofview.Goal.enter begin fun gl -> - let clenv, _ = connect_hint_clenv h gl in + let clenv = connect_hint_clenv h gl in Clenv.res_pf ?with_evars ?with_classes ?flags clenv end diff --git a/tactics/hints.mli b/tactics/hints.mli index d8b6458c27..f0fed75828 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -239,8 +239,7 @@ val wrap_hint_warning_fun : env -> evar_map -> (evar_map -> 'a * evar_map) -> 'a * evar_map (** Variant of the above for non-tactics *) -val connect_hint_clenv - : hint -> Proofview.Goal.t -> clausenv * constr +val fresh_hint : env -> evar_map -> hint -> evar_map * constr val hint_res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic |