Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757

+ un error qui devrait être un anomaly


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

4 files changed, 16 insertions, 4 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index f3ecbd446f..424cb93ef7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -288,7 +288,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
 
 let declare_notation_level ntn level =
   if Gmap.mem ntn !notation_level_map then
-    error ("Notation "^ntn^" is already assigned a level");
+    anomaly ("Notation "^ntn^" is already assigned a level");
   notation_level_map := Gmap.add ntn level !notation_level_map
 
 let level_of_notation ntn =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d3f7cc5f15..2259af67c0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -400,7 +400,7 @@ let is_quantified_hypothesis id g =
 
 let msg_quantified_hypothesis = function
   | NamedHyp id -> 
-      str "hypothesis " ++ pr_id id
+      str "quantified hypothesis named " ++ pr_id id
   | AnonHyp n ->
       int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
       str " non dependent hypothesis"
@@ -411,8 +411,8 @@ let depth_of_quantified_hypothesis red h gl =
     | None ->
         errorlabstrm "lookup_quantified_hypothesis" 
           (str "No " ++ msg_quantified_hypothesis h ++
-	  str " in current goal" ++
-	  if red then str " even after head-reduction" else mt ())
+	  strbrk " in current goal" ++
+	  if red then strbrk " even after head-reduction" else mt ())
 
 let intros_until_gen red h g =
   tclDO (depth_of_quantified_hypothesis red h g) intro g
diff --git a/test-suite/bugs/opened/shouldnotfail/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v
index bde7087865..d9ce546a2b 100644
--- a/test-suite/bugs/opened/shouldnotfail/1740.v
+++ b/test-suite/bugs/closed/shouldsucceed/1740.v
@@ -1,3 +1,6 @@
+(* Check that expansion of alias in pattern-matching compilation is no
+   longer dependent of whether the pattern-matching problem occurs in a
+   typed context or at toplevel (solved from revision 10883) *)
 
 Definition f :=
   fun n m : nat =>
diff --git a/test-suite/bugs/closed/shouldsucceed/1773.v b/test-suite/bugs/closed/shouldsucceed/1773.v
new file mode 100644
index 0000000000..211af89b70
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1773.v
@@ -0,0 +1,9 @@
+(* An occur-check test was done too early *)
+
+Goal forall B C : nat -> nat -> Prop, forall k,
+  (exists A, (forall k', C A k' -> B A k') -> B A k).
+Proof.
+  intros B C k.
+  econstructor.
+  intros X.
+  apply X. (* used to fail here *)