diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-09 20:33:42 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-09 20:33:42 +0000 |
| commit | a814dc7903b1405c195ec6023edef1d5a1b85653 (patch) | |
| tree | 9a9331b7ba3c02a1777dcd537bd75c9663d80817 | |
| parent | 44112550468d281a16e7a22b919fe87991dea624 (diff) | |
f_equal : solve an inefficiency issue (apply vs. simple apply)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11567 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/cc/cctac.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index 84388b1c0..d2df855ee 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -431,6 +431,12 @@ let congruence_tac depth l = (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) cc_fail +(* Beware: reflexivity = constructor 1 = apply refl_equal + might be slow now, let's rather do something equivalent + to a "simple apply refl_equal" *) + +let simple_reflexivity () = apply (Lazy.force _refl_equal) + (* The [f_equal] tactic. It mimics the use of lemmas [f_equal], [f_equal2], etc. @@ -442,7 +448,8 @@ let f_equal gl = let cut_eq c1 c2 = let ty = refresh_universes (pf_type_of gl c1) in tclTHENTRY - (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) reflexivity + (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) + (simple_reflexivity ()) in try match kind_of_term (pf_concl gl) with | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> |