- Add pretty-printers for Idpred, Cpred and transparent_state, used for

  debugging and printing hint databases
- Typeclasses unfold now correctly adds _global_ unfold hints.
- New tactic autosimpl to do simplification using the declared unfold
  hints in given hint databases.
- Work on auto-modulo-some-delta (the declared Unfold constants),
  actually used mostly if the goal contains evars, as Hint_db.map_auto
  does not work up-to any conversions (yet).
- Fix GenMul which was using the old semantics of failing early because
  of variance checks, which is not possible in the new implementation.
- Restrict when reflexive_morphism may be used using an extern tactic.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10842 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 22 insertions, 9 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index e2d3f21c7..4b5b71a19 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -334,10 +334,6 @@ Proof. firstorder. Qed.
 (*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
 (* Proof. simpl_relation. Qed. *)
 
-Instance [ Reflexive A R ] (x : A) => 
-  reflexive_morphism : Morphism R x | 4.
-Proof. firstorder. Qed.
-
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
 Program Instance [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ]  =>
@@ -407,8 +403,24 @@ Inductive normalization_done : Prop := did_normalization.
 Ltac morphism_normalization := 
   match goal with
     | [ _ : normalization_done |- _ ] => fail
+(*     | [ _ : subrelation_done |- _ ] => fail (* avoid useless interleavings. *) *)
     | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
       set(H:=did_normalization) ; eapply @morphism_releq_morphism
   end.
 
 Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
+
+(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
+
+Lemma reflexive_morphism [ Reflexive A R ] (x : A)
+   : Morphism R x.
+Proof. firstorder. Qed.
+
+Ltac morphism_reflexive :=
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail
+    | [ _ : subrelation_done |- _ ] => fail
+    | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
+  end.
+
+Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
\ No newline at end of file
diff --git a/theories/Ints/num/GenMul.v b/theories/Ints/num/GenMul.v
index 5522e41bf..c7ac1ea3e 100644
--- a/theories/Ints/num/GenMul.v
+++ b/theories/Ints/num/GenMul.v
@@ -406,8 +406,9 @@ Section GenMul.
      intros z Hz; rewrite <- Hz; unfold interp_carry; assert (Hz1 := (spec_ww_to_Z z)).
    generalize (spec_w_compare xl xh); case (w_compare xl xh); intros Hxlh;
     try rewrite Hxlh; try rewrite spec_w_0; try (ring; fail).
-   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
-     try rewrite Hylh; try rewrite spec_w_0; try (ring; fail).
+   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh.
+   rewrite Hylh; rewrite spec_w_0; try (ring; fail).
+   rewrite spec_w_0; try (ring; fail). 
    repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c).
    repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    split; auto with zarith.
@@ -425,8 +426,8 @@ Section GenMul.
    rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2;
      repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
    repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
-   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh;
-     try rewrite Hylh; try rewrite spec_w_0; try (ring; fail).
+   generalize (spec_w_compare yl yh); case (w_compare yl yh); intros Hylh.
+   rewrite Hylh; rewrite spec_w_0; try (ring; fail).
    match goal with |- context[ww_add_c ?x ?y] =>
      generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_0;
      intros z1 Hz2
@@ -436,6 +437,7 @@ Section GenMul.
    rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2;
      repeat (rewrite spec_w_sub || rewrite spec_w_mul_c).
    repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
+   rewrite spec_w_0; try (ring; fail).
    repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c).
    repeat rewrite Zmod_small; auto with zarith; try (ring; fail).
    split.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 8116045b6..ac3664054 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -101,7 +101,6 @@ Section Sets_as_an_algebra.
     intros X x H'; red in |- *.
     intros x0 H'0; try assumption.
     elim (classic (x = x0)); intro K; auto with sets.
-    elim K; auto with sets.
   Qed.
   
   Lemma add_soustr_1 :