diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 8 |
4 files changed, 8 insertions, 8 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 4218286b0..f780d1bb5 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -721,7 +721,7 @@ let rec consider_match may_intro introduced available expected gls = try conjunction_arity id gls with Not_found -> error "Matching hypothesis not found." in tclTHENLIST - [Proofview.V82.of_tactic (general_case_analysis false (mkVar id,NoBindings)); + [Proofview.V82.of_tactic (simplest_case (mkVar id)); intron_then nhyps [] (fun l -> consider_match may_intro introduced (List.rev_append l rest_ids) expected)] gls) @@ -1313,7 +1313,7 @@ let end_tac et2 gls = tclSOLVE [Proofview.V82.of_tactic (simplest_elim pi.per_casee)] | ET_Case_analysis,EK_nodep -> tclTHEN - (Proofview.V82.of_tactic (general_case_analysis false (pi.per_casee,NoBindings))) + (Proofview.V82.of_tactic (simplest_case pi.per_casee)) (default_justification (List.map mkVar clauses)) | ET_Induction,EK_nodep -> tclTHENLIST diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 841796ed7..1981fb837 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -976,7 +976,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); - (* observe_tac "h_case" *) (Proofview.V82.of_tactic (general_case_analysis false (mkVar rec_id,NoBindings))); + (* observe_tac "h_case" *) (Proofview.V82.of_tactic (simplest_case (mkVar rec_id))); (Proofview.V82.of_tactic intros_reflexivity)] g ) ] diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 808b2604c..953e1f049 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -80,7 +80,7 @@ let functional_induction with_clean c princl pat = if princ_infos.Tactics.farg_in_concl then [c] else [] in - List.map (fun c -> Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list) + List.map (fun c -> None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list) in let princ' = Some (princ,bindings) in let princ_vars = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 52d3b4a87..5682c2aa4 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -799,7 +799,7 @@ and intros_with_rewrite_aux : tactic = Proofview.V82.of_tactic Tauto.tauto g | Case(_,_,v,_) -> tclTHENSEQ[ - Proofview.V82.of_tactic (general_case_analysis false (v,NoBindings)); + Proofview.V82.of_tactic (simplest_case v); intros_with_rewrite ] g | LetIn _ -> @@ -836,7 +836,7 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (snd (destApp (pf_concl g))).(2) with | Case(_,_,v,_) -> tclTHENSEQ[ - Proofview.V82.of_tactic (general_case_analysis false (v,NoBindings)); + Proofview.V82.of_tactic (simplest_case v); Proofview.V82.of_tactic intros; observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] @@ -855,7 +855,7 @@ let rec reflexivity_with_destruct_cases g = if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp id);thin [id];intros_with_rewrite] g + then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) @@ -1013,7 +1013,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); Proofview.V82.of_tactic (Simple.intro graph_principle_id); observe_tac "" (tclTHEN_i - (observe_tac "elim" (Proofview.V82.of_tactic ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))) + (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g |