diff options
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 47 |
1 files changed, 31 insertions, 16 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 0ab426cd2..328d45991 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -32,7 +32,7 @@ let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_tr let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 || occur_existential t2 then - tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl + tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl else exact_check c gl let assumption id = e_give_exact (mkVar id) @@ -86,8 +86,12 @@ let rec prolog l n gl = let prol = (prolog l (n-1)) in (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl +let out_term = function + | IsConstr (c, _) -> c + | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr) + let prolog_tac l n gl = - let l = List.map (prepare_hint (pf_env gl)) l in + let l = List.map (fun x -> out_term (pf_apply (prepare_hint false) gl x)) l in let n = match n with | ArgArg n -> n @@ -110,11 +114,19 @@ open Unification let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) -let unify_e_resolve flags (c,clenv) gls = - let clenv' = connect_clenv gls clenv in +let unify_e_resolve poly flags (c,clenv) gls = + let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv + else clenv, Univ.empty_level_subst in + let clenv' = connect_clenv gls clenv' in let _ = clenv_unique_resolver ~flags clenv' gls in - Tactics.Simple.eapply c gls - + Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c) gls + +let e_exact poly flags (c,clenv) = + let clenv', subst = + if poly then Clenv.refresh_undefined_univs clenv + else clenv, Univ.empty_level_subst + in e_give_exact ~flags (Vars.subst_univs_level_constr subst c) + let rec e_trivial_fail_db db_list local_db goal = let tacl = registered_e_assumption :: @@ -141,15 +153,15 @@ and e_my_find_search db_list local_db hdc concl = List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in let tac_of_hint = - fun (st, {pri=b; pat = p; code=t}) -> + fun (st, {pri = b; pat = p; code = t; poly = poly}) -> (b, let tac = match t with - | Res_pf (term,cl) -> unify_resolve st (term,cl) - | ERes_pf (term,cl) -> unify_e_resolve st (term,cl) - | Give_exact (c) -> e_give_exact c + | Res_pf (term,cl) -> unify_resolve poly st (term,cl) + | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) + | Give_exact (c,cl) -> e_exact poly st (c,cl) | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN (unify_e_resolve st (term,cl)) + tclTHEN (unify_e_resolve poly st (term,cl)) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast) @@ -162,13 +174,13 @@ and e_trivial_resolve db_list local_db gl = try priority (e_my_find_search db_list local_db - (fst (head_constr_bound gl)) gl) + (head_constr_bound gl) gl) with Bound | Not_found -> [] let e_possible_resolve db_list local_db gl = try List.map snd (e_my_find_search db_list local_db - (fst (head_constr_bound gl)) gl) + (head_constr_bound gl) gl) with Bound | Not_found -> [] let find_first_goal gls = @@ -363,6 +375,9 @@ let e_search_auto debug (in_depth,p) lems db_list gl = pr_info_nop d; error "eauto: search failed" +(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) +(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) + let eauto_with_bases ?(debug=Off) np lems db_list = tclTRY (e_search_auto debug np lems db_list) @@ -494,8 +509,8 @@ let unfold_head env (ids, csts) c = (match Environ.named_body id env with | Some b -> true, b | None -> false, c) - | Const cst when Cset.mem cst csts -> - true, Environ.constant_value env cst + | Const (cst,u as c) when Cset.mem cst csts -> + true, Environ.constant_value_in env c | App (f, args) -> (match aux f with | true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args)) @@ -558,7 +573,7 @@ TACTIC EXTEND autounfoldify | [ "autounfoldify" constr(x) ] -> [ Proofview.V82.tactic ( let db = match kind_of_term x with - | Const c -> Label.to_string (con_label c) + | Const (c,_) -> Label.to_string (con_label c) | _ -> assert false in autounfold ["core";db] onConcl )] |