Améliorations de l'affichage des coercions suggérées par Georges :

- Suppression d'un hack bancal qui permettait d'afficher des notations
  dont les arguments du premier niveau applicatif n'étaient pas
  syntaxiquement entourés de coercions dans la définition de la
  notation alors qu'ils ne pouvaient que l'être dans les termes
  effectifs (ex: 'Notation ... := (true /\ True)' pouvait être reconnu
  malgré l'absence de la coercion de bool vers Prop).

- Propagation de l'information "in context" aux branches des
  if/let/match par symmétrie avec l'inférence de type qui propage
  l'information EXTERNE de type vers les branches (stratégie moins
  "défensive" pour la suppression des coercions).



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

1 files changed, 7 insertions, 12 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 304ac5d78..a3393863b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -544,15 +544,10 @@ let rec remove_coercions inctx = function
 	      (* 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) =
-                (* Recursively remove the head coercions *)
-                match remove_coercions true a with
-                  | RApp (_,a,l') -> a,l'@l
-                  | a -> a,l in
-              if l = [] then a
-              else
-                (* Recursively remove coercions in arguments *)
-                RApp (loc,a,List.map (remove_coercions true) l)
+              (* Recursively remove the head coercions *)
+              (match remove_coercions true a with
+              | RApp (_,a,l') -> RApp (loc,a,l'@l)
+              | a -> RApp (loc,a,l))
 	  | _ -> c
       with Not_found -> c)
   | c -> c
@@ -694,7 +689,7 @@ let rec extern inctx scopes vars r =
 	    | Name id -> RVar (dummy_loc,id)) nal in
 	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
 	  (extern_typ scopes vars t)) x))) tml in
-      let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in 
+      let eqns = List.map (extern_eqn inctx scopes vars) eqns in 
       CCases (loc,sty,rtntypopt',tml,eqns)
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
@@ -702,13 +697,13 @@ let rec extern inctx scopes vars r =
         (Option.map (fun _ -> na) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
-        extern false scopes (List.fold_left add_vname vars nal) b)
+        extern inctx scopes (List.fold_left add_vname vars nal) b)
 
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
         (Option.map (fun _ -> na) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
-        sub_extern false scopes vars b1, sub_extern false scopes vars b2)
+        sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
   | RRec (loc,fk,idv,blv,tyv,bv) ->
       let vars' = Array.fold_right Idset.add idv vars in