Revision 12439 continued, printing part (notations to names behave

like the name they refer to).
Fixing buggy test-suite implicit.v


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

3 files changed, 20 insertions, 15 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0e61905c7c..0f3ed9511b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -785,13 +785,22 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
       let loc = Rawterm.loc_of_rawconstr t in
       try
 	(* Adjusts to the number of arguments expected by the notation *)
-	let (t,args) = match t,n with
-	  | RApp (_,(RRef _ as f),args), Some n when List.length args >= n ->
+	let (t,args,argsscopes,argsimpls) = match t,n with
+	  | RApp (_,(RRef (_,ref) as f),args), Some n
+	      when List.length args >= n ->
 	      let args1, args2 = list_chop n args in
-	      (if n = 0 then f else RApp (dummy_loc,f,args1)), args2
-	  | RApp (_,(RRef _ as f),args), None -> f, args
-	  | RRef _, Some 0 -> RApp (dummy_loc,t,[]), []
-          | _, None -> t,[]
+	      let subscopes =
+		try list_skipn n (find_arguments_scope ref) with _ -> [] in
+	      let impls =
+		try list_skipn n (implicits_of_global ref) with _ -> [] in
+	      (if n = 0 then f else RApp (dummy_loc,f,args1)),
+	      args2, subscopes, impls
+	  | RApp (_,(RRef (_,ref) as f),args), None ->
+	      let subscopes = find_arguments_scope ref in
+	      let impls = implicits_of_global ref in
+	      f, args, subscopes, impls
+	  | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], []
+          | _, None -> t, [], [], []
           | _ -> raise No_match in
 	(* Try matching ... *)
 	let subst,substlist = match_aconstr t pat in
@@ -824,9 +833,8 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 	      if l = [] then a else CApp (loc,(None,a),l) in
  	if args = [] then e
 	else
-	  (* TODO: compute scopt for the extra args, in case, head is a ref *)
-	  explicitize loc false [] (None,e)
-	  (List.map (extern true allscopes vars) args)
+	  let args = extern_args (extern true) scopes vars args argsscopes in
+	  explicitize loc false argsimpls (None,e) args
       with
 	  No_match -> extern_symbol allscopes vars t rules
 
diff --git a/lib/util.ml b/lib/util.ml
index 794f1a6ac0..d71912289d 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -850,7 +850,7 @@ let list_lastn n l =
 
 let rec list_skipn n l = match n,l with
   | 0, _ -> l
-  | _, [] -> failwith "list_fromn"
+  | _, [] -> failwith "list_skipn"
   | n, _::l -> list_skipn (pred n) l
 
 let rec list_addn n x l =
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index c6d0a6dd2a..59e1a9352f 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -14,6 +14,7 @@ Infix "#" := op (at level 70).
 Check (forall x : A, x # x).
 
 (* Example submitted by Christine *)
+
 Record stack : Type :=
   {type : Set; elt : type; empty : type -> bool; proof : empty elt = true}.
 
@@ -21,7 +22,7 @@ Check
   (forall (type : Set) (elt : type) (empty : type -> bool),
    empty elt = true -> stack).
 
-(* Nested sections and manual implicit arguments *)
+(* Nested sections and manual/automatic implicit arguments *)
 
 Variable op' : forall A : Set, A -> A -> Set.
 Variable op'' : forall A : Set, A -> A -> Set.
@@ -60,10 +61,6 @@ Check (eq1 0 0).
 Check (eq2 0 0).
 Check (eq3 nat 0 0).
 
-(* Test discharge on automatic implicit arguments *)
-
-Check (op' 0 0).
-
 (* Example submitted by Frédéric (interesting in v8 syntax) *)
 
 Parameter f : nat -> nat * nat.