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

3 files changed, 10 insertions, 14 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
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9b3268930c..f5ad4172c1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -44,8 +44,6 @@ let for_grammar f x =
 
 let variables_bind = ref false
 
-let insert_maximal_implicit = ref false
-
 (**********************************************************************)
 (* Internalisation errors                                             *)
 
@@ -1035,10 +1033,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	    let eargs' = List.remove_assoc id eargs in
 	    intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
 	  with Not_found ->
-	  if rargs=[] & eargs=[] & not !insert_maximal_implicit &
-	    not (List.for_all is_status_implicit impl') then
-	    (* Less regular arguments than expected: don't complete *)
-	    (* with implicit arguments *)
+	  if rargs=[] & eargs=[] & not (maximal_insertion_of imp) then
+            (* Less regular arguments than expected: complete *)
+            (* with implicit arguments if maximal insertion is set *)
 	    []
 	  else
 	    RHole (set_hole_implicit (n,get_implicit_name n l) c) :: 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index d7634d6e09..edbf9fb62a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -47,8 +47,6 @@ type full_implicits_env = identifier list * implicits_env
 
 type ltac_sign = identifier list * unbound_ltac_var_map
 
-val insert_maximal_implicit : bool ref
-
 (*s Internalisation performs interpretation of global names and notations *)
 
 val intern_constr : evar_map -> env -> constr_expr -> rawconstr