* Ajout du traducteur nouvelle syntaxe *

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

4 files changed, 5 insertions, 5 deletions

diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v
index b4367fd309..17895b4624 100644
--- a/contrib/correctness/Arrays.v
+++ b/contrib/correctness/Arrays.v
@@ -71,4 +71,5 @@ Tactic Definition ArrayAccess i j H :=
 
 (* Symbolic notation for access *)
 
-Notation "# t [ c ]" := (access t c) (at level 0, t ident).
+Notation "# t [ c ]" := (access t c) (at level 0, t ident)
+  V8only (at level 10, t at level 0).
diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v
index 9dc9d066ab..73179ed1e1 100644
--- a/contrib/correctness/Sorted.v
+++ b/contrib/correctness/Sorted.v
@@ -15,6 +15,7 @@ Require ArrayPermut.
 
 Require ZArithRing.
 Require Omega.
+Import Z_scope.
 
 Set Implicit Arguments.
 
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index dbaf419588..e3028ffb04 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -226,8 +226,7 @@ let register id n =
   Penv.register id id'
 
 let correctness_hook _ ref = 
-  let ctx = Global.named_context () in
-  let pf_id = basename (Nametab.sp_of_global (Some ctx) ref) in
+  let pf_id = Nametab.id_of_global ref in
   register pf_id None
 
 let correctness s p opttac =
diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml
index e390e156da..e5af703d26 100644
--- a/contrib/correctness/pwp.ml
+++ b/contrib/correctness/pwp.ml
@@ -115,8 +115,7 @@ let is_bool = function
   | TypePure c ->
       (match kind_of_term (strip_outer_cast c) with
 	 | Ind op ->
-	     let sign = Global.named_context () in
-             string_of_id (id_of_global (Some sign) (IndRef op)) = "bool"
+             string_of_id (id_of_global (IndRef op)) = "bool"
 	 | _ -> false)
   | _ -> false