Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la suppression des coercions permet aussi d'afficher un nombre, on choisit l'affichage qui n'introduit pas de délimiteurs si possible (exemple: avec 'Zpos 2', si Zpos est une coercion, on peut effacer la coercion et afficher 2 dans le type positive, ou bien garder la coercion afficher 'Zpos 2' comme 2 dans Z; dans certains cas - cf 4CT - il n'y a pas d'afficheur qui gère la coercion et il faut la retirer avant d'appliquer l'afficheur de nombre le plus interne)

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

1 files changed, 24 insertions, 9 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ffd598cd1..006d9bc2f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -583,18 +583,38 @@ let rec share_fix_binders n rbl ty def =
     | _ -> List.rev rbl, ty, def
 
 (**********************************************************************)
+(* mapping rawterms to numerals (in presence of coercions, choose the *)
+(* one with no delimiter if possible)                                 *)
+
+let extern_possible_prim_token scopes r =
+  try
+    let (sc,n) = uninterp_prim_token r in
+    match availability_of_prim_token sc (make_current_scopes scopes) with
+    | None -> None
+    | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
+  with No_match ->
+    None
+
+let extern_optimal_prim_token scopes r r' =
+  let c = extern_possible_prim_token scopes r in
+  let c' = if r==r' then None else extern_possible_prim_token scopes r' in
+  match c,c' with
+  | Some n, (Some (CDelimiters _) | None) | _, Some n -> n
+  | _ -> raise No_match
+
+(**********************************************************************)
 (* mapping rawterms to constr_expr                                    *)
 
 let rec extern inctx scopes vars r =
-  let r = remove_coercions inctx r in
+  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)
+    extern_optimal_prim_token scopes r r'
   with No_match ->
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
-    extern_symbol scopes vars r (uninterp_notations r)
-  with No_match -> match r with
+    extern_symbol scopes vars r' (uninterp_notations r')
+  with No_match -> match r' with
   | RRef (loc,ref) ->
       extern_global loc (implicits_of_global ref)
         (extern_reference loc vars ref)
@@ -763,11 +783,6 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
    extern inctx scopes vars c)
 
-and extern_prim_token loc scopes (sc,p) =
-  match availability_of_prim_token sc (make_current_scopes scopes) with
-  | None -> raise No_match
-  | Some key -> insert_delimiters (CPrim (loc,p)) key
-
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->