diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 1 | ||||
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/hiddentac.ml | 6 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 116 | ||||
| -rw-r--r-- | tactics/tactics.mli | 8 | ||||
| -rw-r--r-- | theories/Classes/Init.v | 2 |
7 files changed, 78 insertions, 59 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 4e910935a..7b654b74b 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -375,6 +375,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function (xlate_formula f, List.map xlate_formula_expl l')) | CApp(_, (_,f), l) -> CT_appc(xlate_formula f, xlate_formula_expl_ne_list l) + | CRecord (_,_,_) -> xlate_error "CRecord: TODO" | CCases (_, _, _, [], _) -> assert false | CCases (_, _, ret_type, tm::tml, eqns)-> CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm, diff --git a/tactics/auto.ml b/tactics/auto.ml index e9ec90ec3..42d74f9ed 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -724,7 +724,7 @@ let unify_resolve_nodelta (c,clenv) gls = let unify_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false ~flags clenv' gls in - h_apply true false [c,NoBindings] gls + h_apply true false [inj_open c,NoBindings] gls (* builds a hint database from a constr signature *) diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 1acc4880c..6498c3542 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -40,7 +40,7 @@ let h_exact_no_check c = let h_vm_cast_no_check c = abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c) let h_apply simple ev cb = - abstract_tactic (TacApply (simple,ev,List.map inj_open_wb cb)) + abstract_tactic (TacApply (simple,ev,cb)) (apply_with_ebindings_gen simple ev cb) let h_elim ev cb cbo = abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo)) @@ -131,8 +131,8 @@ let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c) let h_transitivity c = abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c) -let h_simplest_apply c = h_apply false false [c,NoBindings] -let h_simplest_eapply c = h_apply false true [c,NoBindings] +let h_simplest_apply c = h_apply false false [inj_open c,NoBindings] +let h_simplest_eapply c = h_apply false true [inj_open c,NoBindings] let h_simplest_elim c = h_elim false (c,NoBindings) None let h_simplest_case c = h_case false (c,NoBindings) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 8d15f864c..938befa49 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -36,7 +36,7 @@ val h_exact_no_check : constr -> tactic val h_vm_cast_no_check : constr -> tactic val h_apply : advanced_flag -> evars_flag -> - constr with_ebindings list -> tactic + open_constr with_bindings list -> tactic val h_elim : evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 65082c2ee..be15311b9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -719,52 +719,70 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl = goal. If this fails, then the head constant will be unfolded step by step. *) let concl_nprod = nb_prod (pf_concl gl) in + let evm, c = c in + let origsigm = gl.sigma in + let check_evars sigm = + let rest = + Evd.fold (fun ev evi acc -> + if Evd.mem sigm ev && not (Evd.mem origsigm ev) && not (Evd.is_defined sigm ev) then + Evd.add acc ev evi + else acc) evm Evd.empty + in + if not (rest = Evd.empty) then + errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ fnl () ++ + pr_evar_map rest) + in let rec try_main_apply c gl = - let thm_ty0 = nf_betaiota (pf_type_of gl c) in - let try_apply thm_ty nprod = - let n = nb_prod thm_ty - nprod in - if n<0 then error "Applied theorem has not enough premisses."; - let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in - Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in - try try_apply thm_ty0 concl_nprod - with PretypeError _|RefinerError _|UserError _|Failure _ as exn -> - let rec try_red_apply thm_ty = - try - (* Try to head-reduce the conclusion of the theorem *) - let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in - try try_apply red_thm concl_nprod - with PretypeError _|RefinerError _|UserError _|Failure _ -> - try_red_apply red_thm - with Redelimination -> - (* Last chance: if the head is a variable, apply may try - second order unification *) - try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit - with PretypeError _|RefinerError _|UserError _|Failure _|Exit -> - if with_destruct then - try - let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in - match match_with_conjunction (snd (decompose_prod t)) with - | Some _ -> - let n = (mis_constr_nargs mind).(0) in - let sort = elimination_sort_of_goal gl in - let elim = pf_apply make_case_gen gl mind sort in - tclTHENLAST - (general_elim with_evars (c,NoBindings) (elim,NoBindings)) - (tclTHENLIST [ - tclDO n intro; - tclLAST_NHYPS n (fun l -> - tclFIRST - (List.map (fun id -> - tclTHEN (try_main_apply (mkVar id)) (thin l)) l)) - ]) gl - | None -> - raise Exit - with RefinerError _|UserError _|Exit -> raise exn - else - raise exn - in - try_red_apply thm_ty0 in - try_main_apply c gl + let thm_ty0 = nf_betaiota (pf_type_of gl c) in + let try_apply thm_ty nprod = + let n = nb_prod thm_ty - nprod in + if n<0 then error "Applied theorem has not enough premisses."; + let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in + let res = Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in + if not with_evars then check_evars (fst res).sigma; + res + in + try try_apply thm_ty0 concl_nprod + with PretypeError _|RefinerError _|UserError _|Failure _ as exn -> + let rec try_red_apply thm_ty = + try + (* Try to head-reduce the conclusion of the theorem *) + let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in + try try_apply red_thm concl_nprod + with PretypeError _|RefinerError _|UserError _|Failure _ -> + try_red_apply red_thm + with Redelimination -> + (* Last chance: if the head is a variable, apply may try + second order unification *) + try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit + with PretypeError _|RefinerError _|UserError _|Failure _|Exit -> + if with_destruct then + try + let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + match match_with_conjunction (snd (decompose_prod t)) with + | Some _ -> + let n = (mis_constr_nargs mind).(0) in + let sort = elimination_sort_of_goal gl in + let elim = pf_apply make_case_gen gl mind sort in + tclTHENLAST + (general_elim with_evars (c,NoBindings) (elim,NoBindings)) + (tclTHENLIST [ + tclDO n intro; + tclLAST_NHYPS n (fun l -> + tclFIRST + (List.map (fun id -> + tclTHEN (try_main_apply (mkVar id)) (thin l)) l)) + ]) gl + | None -> + raise Exit + with RefinerError _|UserError _|Exit -> raise exn + else + raise exn + in try_red_apply thm_ty0 + in + if evm = Evd.empty then try_main_apply c gl + else + tclTHEN (tclEVARS (Evd.merge gl.sigma evm)) (try_main_apply c) gl let rec apply_with_ebindings_gen b e = function | [] -> @@ -778,13 +796,13 @@ let apply_with_ebindings cb = apply_with_ebindings_gen false false [cb] let eapply_with_ebindings cb = apply_with_ebindings_gen false true [cb] let apply_with_bindings (c,bl) = - apply_with_ebindings (c,inj_ebindings bl) + apply_with_ebindings (inj_open c,inj_ebindings bl) let eapply_with_bindings (c,bl) = - apply_with_ebindings_gen false true [c,inj_ebindings bl] + apply_with_ebindings_gen false true [inj_open c,inj_ebindings bl] let apply c = - apply_with_ebindings (c,NoBindings) + apply_with_ebindings (inj_open c,NoBindings) let apply_list = function | c::l -> apply_with_bindings (c,ImplicitBindings l) @@ -1009,7 +1027,7 @@ let constructor_tac with_evars expctdnumopt i lbind gl = Array.length (snd (Global.lookup_inductive mind)).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; let cons = mkConstruct (ith_constructor_of_inductive mind i) in - let apply_tac = general_apply true false with_evars (cons,lbind) in + let apply_tac = general_apply true false with_evars (inj_open cons,lbind) in (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 99f2140dd..b2bd508ce 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -181,15 +181,15 @@ val bring_hyps : named_context -> tactic val apply : constr -> tactic val apply_without_reduce : constr -> tactic val apply_list : constr list -> tactic - + val apply_with_ebindings_gen : - advanced_flag -> evars_flag -> constr with_ebindings list -> tactic + advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic val apply_with_bindings : constr with_bindings -> tactic val eapply_with_bindings : constr with_bindings -> tactic -val apply_with_ebindings : constr with_ebindings -> tactic -val eapply_with_ebindings : constr with_ebindings -> tactic +val apply_with_ebindings : open_constr with_ebindings -> tactic +val eapply_with_ebindings : open_constr with_ebindings -> tactic val cut_and_apply : constr -> tactic diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 0bd9f95dd..8b4cac5f4 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -34,7 +34,7 @@ Class Unconvertible (A : Type) (a b : A). Ltac unconvertible := match goal with | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible" - | |- _ => apply Build_Unconvertible + | |- _ => eapply Build_Unconvertible end. Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file |