diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 54 |
1 files changed, 37 insertions, 17 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 46274f83..a6b53d76 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -72,27 +72,44 @@ let auto_flags_of_state st = (* Try unification with the precompiled clause, then use registered Apply *) -let unify_resolve_nodelta poly (c,clenv) = +let connect_hint_clenv poly (c, _, ctx) clenv gl = + (** [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 = Proofview.Goal.sigma 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 poly then + (** Refresh the instance of the hint *) + let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in + let map c = Vars.subst_univs_level_constr subst c in + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in + (** FIXME: We're being inefficient here because we substitute the whole + evar map instead of just its metas, which are the only ones + mentioning the old universes. *) + Clenv.map_clenv map clenv, map 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 + +let unify_resolve poly flags ((c : raw_hint), clenv) = Proofview.Goal.nf_enter begin fun gl -> - let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in - let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in - let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags:auto_unif_flags clenv' gl) gl in - Clenvtac.clenv_refine false clenv'' + let clenv, c = connect_hint_clenv poly c clenv gl in + let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in + Clenvtac.clenv_refine false clenv end -let unify_resolve poly flags (c,clenv) = - Proofview.Goal.nf_enter begin fun gl -> - let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in - let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in - let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv' gl) gl in - Clenvtac.clenv_refine false clenv'' - end +let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h let unify_resolve_gen poly = function | None -> unify_resolve_nodelta poly | Some flags -> unify_resolve poly flags let exact poly (c,clenv) = + let (c, _, _) = c in let ctx, c' = if poly then let evd', subst = Evd.refresh_undefined_universes clenv.evd in @@ -131,7 +148,7 @@ let conclPattern concl pat tac = try Proofview.tclUNIT (Constr_matching.matches env sigma pat concl) with Constr_matching.PatternMatchingFailure -> - Proofview.tclZERO (UserError ("conclPattern",str"conclPattern")) + Tacticals.New.tclZEROMSG (str "conclPattern") in Proofview.Goal.enter (fun gl -> let env = Proofview.Goal.env gl in @@ -309,7 +326,8 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in let hyp = Context.map_named_declaration nf decl in let hintl = make_resolve_hyp env sigma hyp - in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db) + in trivial_fail_db dbg mod_delta db_list + (Hint_db.add_list env sigma hintl local_db) end) in Proofview.Goal.enter begin fun gl -> @@ -377,7 +395,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) | Extern tacast -> conclPattern concl p tacast in - tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic) + tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic) and trivial_resolve dbg mod_delta db_list local_db cl = try @@ -438,7 +456,9 @@ let possible_resolve dbg mod_delta db_list local_db cl = with Not_found -> [] let extend_local_db decl db gl = - Hint_db.add_list (make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) decl) db + let env = Tacmach.New.pf_env gl in + let sigma = Proofview.Goal.sigma gl in + Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db (* Introduce an hypothesis, then call the continuation tactic [kont] with the hint db extended with the so-obtained hypothesis *) @@ -458,7 +478,7 @@ let search d n mod_delta db_list local_db = (* spiwack: the test of [n] to 0 must be done independently in each goal. Hence the [tclEXTEND] *) Proofview.tclEXTEND [] begin - if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else + if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else Tacticals.New.tclORELSE0 (dbg_assumption d) (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) ( Proofview.Goal.enter begin fun gl -> |