- Ajout possibilité de lancer ocamldebug sur coqide

- Correction bug #1815 sur "coqide dir_inexistant/nom_fichier"
- Tests oubliés de la révision 11438 (amélioration affichage coercions)



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

2 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 6c69c097dd..acfcd5aff0 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -50,6 +50,8 @@ Nil
      : forall A : Type, list A
 NIL:list nat
      : list nat
+(false && I 3)%bool /\ I 6
+     : Prop
 [|1, 2, 3; 4, 5, 6|]
      : Z * Z * Z * (Z * Z * Z)
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index f19ba998fa..4577f0e196 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -130,6 +130,18 @@ Check Nil.
 Notation NIL := nil.
 Check NIL : list nat.
 
+
+(**********************************************************************)
+(* Test printing of notation with coercions in scope of a coercion    *)
+
+Open Scope nat_scope.
+
+Coercion is_true := fun b => b=true.
+Coercion of_nat n := match n with 0 => true | _ => false end.
+Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
+
+Check (false && I 3)%bool /\ I 6.
+
 (**********************************************************************)
 (* Check notations with several recursive patterns                    *)