diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-20 13:58:03 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-20 13:58:03 +0000 |
| commit | d516c922b388411c46f9046ffe6df99b4061f33b (patch) | |
| tree | 83ec65f70f0f0df2c528179fa722a0cc53f39e8a /theories/Program | |
| parent | 45b27e6f0a304cfd8fee31e901151c6ed7bac1bf (diff) | |
Use unfold directly in unfold_equations. Fixes test-suite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12246 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 6c4fe71fc..f35dc7adc 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -336,16 +336,11 @@ Proof. intros. injection H. intros ; auto. Defined. Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B (refl_equal x) -> (Π p : x = x, B p). Proof. intros. rewrite (UIP_refl A). assumption. Defined. -(** This hint database and the following tactic can be used with [autosimpl] to - unfold everything to [eq_rect]s. *) - -Hint Unfold solution_left solution_right deletion simplification_heq - simplification_existT1 simplification_existT2 - eq_rect_r eq_rec eq_ind : equations. - (** Simply unfold as much as possible. *) -Ltac unfold_equations := repeat progress autosimpl with equations. +Ltac unfold_equations := + unfold solution_left, solution_right, deletion, simplification_heq, + simplification_existT1, simplification_existT2, eq_rect_r, eq_rec, eq_ind. (** The tactic [simplify_equations] is to be used when a program generated using [Equations] is in the goal. It simplifies it as much as possible, possibly using [K] if needed. *) |