From 819029226c334030a540ed7570bc423c4463c6b4 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 16:56:46 +0000 Subject: rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite rewrite_db fails if nothing has been rewritten, and it only performs *one* top-down pass. For the moment, use (repeat rewrite_db) for emulating more closely autorewrite. Btw, let's make Himsg.explain_ltac_call_trace robust wrt TacExtend with fun(ny) parts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15522 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/EnvRing.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/micromega/EnvRing.v') diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index c172157f1..e1424bb10 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -617,7 +617,8 @@ Qed. (morph_opp CRmorph) : Esimpl. - Ltac Esimpl := autorewrite with Esimpl; rsimpl; simpl. + (* Quicker than autorewrite with Esimpl :-) *) + Ltac Esimpl := try rewrite_db Esimpl; rsimpl; simpl. Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c]. Proof. -- cgit v1.2.3