Affichage forcé des implicites contextuels si pas de contexte connu

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

2 files changed, 19 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 472b636a8f..3448a18dea 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -154,14 +154,15 @@ let occur_name na aty =
     | Anonymous -> false
 
 (* Implicit args indexes are in ascending order *)
-let explicitize loc impl f args =
+(* inctx is useful only if there is a last argument to be deduced from ctxt *)
+let explicitize loc inctx impl f args =
   let n = List.length args in
   let rec exprec q = function
     | a::args, imp::impl when is_status_implicit imp ->
         let tail = exprec (q+1) (args,impl) in
         let visible =
           (!print_implicits & !print_implicits_explicit_args)
-          or not (is_inferable_implicit n imp) in
+          or not (is_inferable_implicit inctx n imp) in
         if visible then (a,Some q) :: tail else tail
     | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
     | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*)
@@ -185,14 +186,14 @@ let rec skip_coercion dest_ref (f,args as app) =
 	| None -> app
     with Not_found -> app
 
-let extern_app loc impl f args =
+let extern_app loc inctx impl f args =
   if !print_implicits &
     not !print_implicits_explicit_args &
     List.exists is_status_implicit impl
   then 
     CAppExpl (loc, f, args)
   else
-    explicitize loc impl (CRef f) args
+    explicitize loc inctx impl (CRef f) args
 
 let rec extern_args extern scopes env args subscopes =
   match args with
@@ -232,16 +233,16 @@ let rec extern inctx scopes vars r =
 	 | RRef (loc,ref) ->
 	     let subscopes = Symbols.find_arguments_scope ref in
 	     let args = extern_args (extern true) scopes vars args subscopes in
-	     extern_app loc (implicits_of_global_out ref)
+	     extern_app loc inctx (implicits_of_global_out ref)
                (extern_reference loc vars ref)
 	       args
 	 | RVar (loc,id) -> (* useful for translation of inductive *)
 	     let args = List.map (extern true scopes vars) args in
-	     extern_app loc (get_temporary_implicits_out id)
+	     extern_app loc inctx (get_temporary_implicits_out id)
 	       (Ident (loc,id))
 	       args
 	 | _       -> 
-	     explicitize loc [] (extern inctx scopes vars f)
+	     explicitize loc inctx [] (extern false scopes vars f)
                (List.map (extern true scopes vars) args))
 
   | RProd (loc,Anonymous,t,c) ->
@@ -365,7 +366,8 @@ and extern_symbol scopes vars t = function
           | SynDefRule kn ->
               CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in
  	if args = [] then e 
-	else explicitize loc [] e (List.map (extern true scopes vars) args)
+	else explicitize loc false [] e 
+	  (List.map (extern true scopes vars) args)
       with
 	  No_match -> extern_symbol scopes vars t rules
 
@@ -416,16 +418,17 @@ let rec extern_pattern tenv vars env = function
       let args = List.map (extern_pattern tenv vars env) args in
       (match f with
 	 | PRef ref ->
-	     extern_app loc (implicits_of_global ref)
+	     extern_app loc false (implicits_of_global ref)
                (extern_reference loc vars ref)
 	       args
-	 | _       -> explicitize loc [] (extern_pattern tenv vars env f) args)
+	 | _       ->
+	     explicitize loc false [] (extern_pattern tenv vars env f) args)
 
   | PSoApp (n,args) ->
       let args = List.map (extern_pattern tenv vars env) args in
       (* [-n] is the trick to embed a so patten into a regular application *)
       (* see constrintern.ml and g_constr.ml4 *)
-      explicitize loc [] (CMeta (loc,-n)) args
+      explicitize loc false [] (CMeta (loc,-n)) args
 
   | PProd (Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ffed01a34e..1032b0116d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -180,6 +180,10 @@ let intern_reference env lvar = function
       (* For old ast syntax compatibility *)
       if (string_of_id id).[0] = '$' then RVar (loc,id),[],[] else
       (* End old ast syntax compatibility *)
+      (* Pour traduction des implicites d'inductifs et points-fixes *)
+      try RVar (loc,id), List.assoc id !temporary_implicits_in, []
+      with Not_found ->
+      (* Fin pour traduction *)
       try intern_var env lvar loc id
       with Not_found -> 
       try intern_qualid loc (make_short_qualid id)
@@ -187,9 +191,7 @@ let intern_reference env lvar = function
 	(* Extra allowance for grammars *)
 	if !interning_grammar then begin
 	  set_var_scope loc id env lvar;
-	  RVar (loc,id), 
-	  (try List.assoc id !temporary_implicits_in with Not_found -> []),
-	  []
+	  RVar (loc,id), [], []
 	end
 	else raise e