Nouveaux changements autour des implicites (notamment suite à

discussion avec Georges)

- La notion d'insertion maximale n'est plus globale mais attachée à
  chaque implicite
- Correction de petits bugs dans le calcul des implicites
- Raffinement de la notion "sous contexte" pour l'affichage des coercions



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

1 files changed, 7 insertions, 6 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 537978269c..771a0b299d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -563,16 +563,17 @@ let rec extern_args extern scopes env args subscopes =
 
 let rec remove_coercions inctx = function
   | RApp (loc,RRef (_,r),args) as c
-      when inctx & not (!Options.raw_print or !print_coercions)
+      when  not (!Options.raw_print or !print_coercions)
       ->
+      let nargs = List.length args in
       (try match Classops.hide_coercion r with
-	  | Some n when n < List.length args ->
+	  | Some n when n < nargs && (inctx or n+1 < nargs) ->
 	      (* We skip a coercion *) 
 	      let l = list_skipn n args in
-              let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
-              let (a,l) =
+	      let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
+	      let (a,l) =
                 (* Recursively remove the head coercions *)
-                match remove_coercions inctx a with
+                match remove_coercions true a with
                   | RApp (_,a,l') -> a,l'@l
                   | a -> a,l in
               if l = [] then a
@@ -886,7 +887,7 @@ let extern_constr_gen at_top scopt env t =
   let avoid = if at_top then ids_of_context env else [] in
   let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   let vars = vars_of_env env in
-  extern (not at_top) (scopt,[]) vars r
+  extern false (scopt,[]) vars r
 
 let extern_constr_in_scope at_top scope env t =
   extern_constr_gen at_top (Some scope) env t