diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-01 17:02:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-01 17:02:00 +0000 |
| commit | 2a4ab4bb5720de115edb7bfbb2124194c1334cc6 (patch) | |
| tree | e4654537cc93bd87c96cb3251af6440a9d583668 /tactics | |
| parent | 4915bfb0184b0d5bd7016bce11743949e5dc31a3 (diff) | |
Correction sur commit précédent : Tactics.cut réduisait de manière inappropriée
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5409 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 9 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
3 files changed, 9 insertions, 7 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 621781187..2f36d0c7e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -135,9 +135,9 @@ let abstract_replace clause c2 c1 unsafe gl = let e = (build_coq_eqT_data ()).eq in let sym = (build_coq_eqT_data ()).sym in let eq = applist (e, [t1;c1;c2]) in - tclTHENS (cut eq) - [tclTHEN intro (onLastHyp (fun id -> - tclTHEN (rewriteRL_clause clause (mkVar id,NoBindings)) (clear [id]))); + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN (rewriteRL_clause clause (mkVar id,NoBindings)) (clear [id])); tclORELSE assumption (tclTRY (tclTHEN (apply sym) assumption))] gl else diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cebc6697e..6444c1756 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -506,19 +506,20 @@ let cut_and_apply c gl = (* Cut tactics *) (**************************) -let true_cut na c gl = +let assert_tac first na c gl = match kind_of_term (hnf_type_of gl c) with | Sort s -> - let id = - match na with + let id = match na with | Anonymous -> let d = match s with Prop _ -> "H" | Type _ -> "X" in fresh_id [] (id_of_string d) gl | Name id -> id in - internal_cut id c gl + (if first then internal_cut else internal_cut_rev) id c gl | _ -> error "Not a proposition or a type" +let true_cut = assert_tac true + let cut c gl = match kind_of_term (hnf_type_of gl c) with | Sort _ -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 27a7d998e..b33bc52f0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -235,6 +235,7 @@ val cut_intro : constr -> tactic val cut_replacing : identifier -> constr -> tactic val cut_in_parallel : constr list -> tactic +val assert_tac : bool -> name -> constr -> tactic val true_cut : name -> constr -> tactic val letin_tac : bool -> name -> constr -> clause -> tactic val forward : bool -> name -> constr -> tactic |