Changement dans le kernel :

   - essai de suppression des dependances debiles. (echec) 
   - Application des patch debian.

Pour ring et field :
   - introduciton de la function de sign et de puissance.
   - Correction de certains bug.
   - supression de ring_replace ....

Pour exact_no_check :
   - ajout de la tactic : vm_cast_no_check (t)
     qui remplace "exact_no_check (t<: type of Goal)"
      (cette version forcais l'evaluation du cast dans le 
       pretypage).




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

1 files changed, 8 insertions, 0 deletions

diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 961101d65..233b40b88 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -17,6 +17,14 @@ Ltac list_fold_right fcons fnil l :=
   | nil => fnil
   end.
 
+Ltac lazy_list_fold_right fcons fnil l :=
+  match l with
+  | (cons ?x ?tl) => 
+       let cont := lazy_list_fold_right fcons fnil in
+       fcons x cont tl
+  | nil => fnil 
+  end.
+
 Ltac list_fold_left fcons fnil l :=
   match l with
   | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl