diff options
| -rw-r--r-- | tactics/inv.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 26 | ||||
| -rw-r--r-- | tactics/tactics.ml | 34 |
3 files changed, 36 insertions, 28 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 140ddf8f43..d41dda23be 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -331,7 +331,9 @@ let projectAndApply thin id eqname names depids gls = substHypIfVariable (* If no immediate variable in the equation, try to decompose it *) (* and apply a trailer which again try to substitute *) - (fun id -> dEqThen false (deq_trailer id) (Some (ElimOnIdent (dummy_loc,id)))) + (fun id -> + dEqThen false (deq_trailer id) + (Some (ElimOnConstr (mkVar id,NoBindings)))) id gls diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a754d1265b..2b050b7ebf 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1606,6 +1606,14 @@ let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in sigma, (loc,cb) +let interp_induction_ident ist gl sigma loc id = + if Tactics.is_quantified_hypothesis id gl then + sigma, ElimOnIdent (loc,id) + else + let c = (RVar (loc,id),Some (CRef (Ident (loc,id)))) in + let c = interp_constr ist (pf_env gl) sigma c in + sigma, ElimOnConstr (c,NoBindings) + let interp_induction_arg ist gl sigma arg = let env = pf_env gl in match arg with @@ -1615,21 +1623,19 @@ let interp_induction_arg ist gl sigma arg = | ElimOnAnonHyp n as x -> sigma, x | ElimOnIdent (loc,id) -> try - sigma, match List.assoc id ist.lfun with - | VInteger n -> ElimOnAnonHyp n - | VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id) - | VConstr ([],c) -> ElimOnConstr (c,NoBindings) + | VInteger n -> + sigma, ElimOnAnonHyp n + | VIntroPattern (IntroIdentifier id) -> + interp_induction_ident ist gl sigma loc id + | VConstr ([],c) -> + sigma, ElimOnConstr (c,NoBindings) | _ -> user_err_loc (loc,"", strbrk "Cannot coerce " ++ pr_id id ++ strbrk " neither to a quantified hypothesis nor to a term.") with Not_found -> - (* Interactive mode *) - if Tactics.is_quantified_hypothesis id gl then - sigma, ElimOnIdent (loc,id) - else - let c = interp_constr ist env sigma (RVar (loc,id),Some (CRef (Ident (loc,id)))) in - sigma, ElimOnConstr (c,NoBindings) + (* We were in non strict (interactive) mode *) + interp_induction_ident ist gl sigma loc id (* Associates variables with values and gives the remaining variables and values *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 59befa7852..0be1e08fc6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -563,8 +563,13 @@ let intros_until = intros_until_gen true let intros_until_n = intros_until_n_gen true let intros_until_n_wored = intros_until_n_gen false +let tclCHECKVAR id gl = ignore (pf_get_hyp gl id); tclIDTAC gl + +let try_intros_until_id_check id = + tclORELSE (intros_until_id id) (tclCHECKVAR id) + let try_intros_until tac = function - | NamedHyp id -> tclTHEN (tclTRY (intros_until_id id)) (tac id) + | NamedHyp id -> tclTHEN (try_intros_until_id_check id) (tac id) | AnonHyp n -> tclTHEN (intros_until_n n) (onLastHypId tac) let rec intros_move = function @@ -582,16 +587,13 @@ let dependent_in_decl a (_,c,t) = or a term with bindings *) let onInductionArg tac = function - | ElimOnConstr (c,lbindc as cbl) -> - if isVar c & lbindc = NoBindings then - tclTHEN (tclTRY (intros_until_id (destVar c))) (tac cbl) - else - tac cbl + | ElimOnConstr cbl -> + tac cbl | ElimOnAnonHyp n -> tclTHEN (intros_until_n n) (onLastHyp (fun c -> tac (c,NoBindings))) | ElimOnIdent (_,id) -> - (*Identifier apart because id can be quantified in goal and not typable*) - tclTHEN (tclTRY (intros_until_id id)) (tac (mkVar id,NoBindings)) + (* A quantified hypothesis *) + tclTHEN (try_intros_until_id_check id) (tac (mkVar id,NoBindings)) (**************************) (* Refinement tactics *) @@ -790,9 +792,10 @@ let elim_in_context with_evars c = function let elim with_evars (c,lbindc as cx) elim = match kind_of_term c with | Var id when lbindc = NoBindings -> - tclTHEN (tclTRY (intros_until_id id)) + tclTHEN (try_intros_until_id_check id) (elim_in_context with_evars cx elim) - | _ -> elim_in_context with_evars cx elim + | _ -> + elim_in_context with_evars cx elim (* The simplest elimination tactic, with no substitutions at all. *) @@ -853,8 +856,8 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl = let general_case_analysis with_evars (c,lbindc as cx) = match kind_of_term c with | Var id when lbindc = NoBindings -> - tclTHEN (tclTRY (intros_until_id id)) - (general_case_analysis_in_context with_evars cx) + tclTHEN (try_intros_until_id_check id) + (general_case_analysis_in_context with_evars cx) | _ -> general_case_analysis_in_context with_evars cx @@ -3177,11 +3180,8 @@ let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls) (* Induction tactics *) (* This was Induction before 6.3 (induction only in quantified premisses) *) -let raw_induct s = tclTHEN (intros_until_id s) (onLastHyp simplest_elim) -let raw_induct_nodep n = tclTHEN (intros_until_n n) (onLastHyp simplest_elim) - -let simple_induct_id hyp = raw_induct hyp -let simple_induct_nodep = raw_induct_nodep +let simple_induct_id s = tclTHEN (intros_until_id s) (onLastHyp simplest_elim) +let simple_induct_nodep n = tclTHEN (intros_until_n n) (onLastHyp simplest_elim) let simple_induct = function | NamedHyp id -> simple_induct_id id |