Bug coercions imbriquees + suppression des coercions avant filtrage sur notations pour respecter le cpmt v7 et la symtrie avec le parsing

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

1 files changed, 28 insertions, 1 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d6074667bf..60e6657d54 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1332,7 +1332,18 @@ let rec skip_coercion dest_ref (f,args as app) =
 		   if n >= List.length args then app
 		   else (* We skip a coercion *) 
 		     let fargs = list_skipn n args in
-	       	     skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+		     (match fargs with
+		       | [] -> assert false
+		       | [RApp(_,a,l)] -> skip_coercion dest_ref (a,l)
+		       | [a] -> (a,[])
+		       | a::l ->
+			   (* If l'<>[], it is because a class reduces to
+			      a functional type, in which case the
+			      synthesis back of the coercion is not possible
+			      without a cast... Moving coercions to 
+			      detyping will be required for a better
+			      analysis *)
+			   app)
 	       | None -> app)
 	| None -> app
     with Not_found -> app
@@ -1365,6 +1376,18 @@ let rec extern_args extern scopes env args subscopes =
 	  | scopt::subscopes -> (scopt,scopes), subscopes in
 	extern argscopes env a :: extern_args extern scopes env args subscopes
 
+let rec remove_coercions_in_application inctx = function
+  | RApp (loc,f,args) ->
+      let f,args = 
+	if inctx then
+	  skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args)
+	else 
+	  (f,args)
+      in
+      if args = [] then f
+      else RApp (loc,f,List.map (remove_coercions_in_application true) args)
+  | c -> c
+
 (**********************************************************************)
 (* mapping rawterms to constr_expr                                    *)
 
@@ -1375,6 +1398,8 @@ let rec extern inctx scopes vars r =
       scopes (Symbols.uninterp_numeral r)
   with No_match ->
 
+  let r = remove_coercions_in_application inctx r in
+
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_symbol scopes vars r (Symbols.uninterp_notations r)
@@ -1390,11 +1415,13 @@ let rec extern inctx scopes vars r =
   | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
 
   | RApp (loc,f,args) ->
+(*
       let (f,args) =
 	if inctx then
 	  skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args)
 	else 
 	  (f,args) in
+*)
       (match f with
 	 | RRef (rloc,ref) ->
 	     let subscopes = Symbols.find_arguments_scope ref in