From 440d6fbe82fd4f4400fde9640b1a0e9bb582fe61 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 4 Jan 2006 20:29:24 +0000
Subject: Suppression des coercions non seulement avant l'affichage des
 notations mais aussi avant l'affichage des notations primitives

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7788 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a8a6b862e8..ffd598cd1a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -586,13 +586,11 @@ let rec share_fix_binders n rbl ty def =
 (* mapping rawterms to constr_expr                                    *)
 
 let rec extern inctx scopes vars r =
+  let r = remove_coercions inctx r in
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_prim_token (loc_of_rawconstr r) scopes (uninterp_prim_token r)
   with No_match ->
-
-  let r = remove_coercions inctx r in
-
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_symbol scopes vars r (uninterp_notations r)
-- 
cgit v1.2.3