Experiment propagation of implicit arguments and arguments scope for

abbreviations of applied references.

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

4 files changed, 15 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index be07cfe7b9..b6744e25d3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,6 +54,8 @@ Notations
 - Abbreviations now use implicit arguments and arguments scopes for printing.
 - Abbreviations to pure names now strictly behave like the name they refer to
   (make redirections of qualified names easier).
+- Abbreviations to applied names now propagate the implicit arguments and
+  arguments scope of the underlying reference.
 - The "where" clause now supports multiple notations per defined object.
 
 Vernacular commands
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cfce965212..85f84b850f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -391,7 +391,6 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
   then
     (set_var_scope loc id genv vars3; RVar (loc,id), [], [], [])
   else
-
   (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
   try
     match List.assoc id unbndltacvars with
@@ -410,8 +409,12 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
 	(* [id] a goal variable *)
 	RVar (loc,id), [], [], []
 
-let find_appl_head_data _ = function
+let find_appl_head_data = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
+  | RApp (_,RRef (_,ref),l) as x when l <> [] ->
+      let n = List.length l in
+      x,list_skipn_at_least n (implicits_of_global ref),
+      list_skipn_at_least n (find_arguments_scope ref),[]
   | x -> x,[],[],[]
 
 let error_not_enough_arguments loc =
@@ -459,14 +462,14 @@ let intern_non_secvar_qualid loc qid intern env args =
 let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
   | Qualid (loc, qid) ->
       let r,args2 = intern_qualid loc qid intern env args in
-	find_appl_head_data lvar r, args2
+      find_appl_head_data r, args2
   | Ident (loc, id) ->
       try intern_var env lvar loc id, args
       with Not_found ->
       let qid = qualid_of_ident id in
       try
 	let r,args2 = intern_non_secvar_qualid loc qid intern env args in
-	find_appl_head_data lvar r, args2
+	find_appl_head_data r, args2
       with e ->
 	(* Extra allowance for non globalizing functions *)
 	if !interning_grammar || unb then
@@ -982,7 +985,7 @@ let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
 let set_hole_implicit i b = function
-  | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i,b))
+  | RRef (loc,r) | RApp (_,RRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b))
   | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b))
   | _ -> anomaly "Only refs have implicits"
 
@@ -1142,7 +1145,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
             | CRef ref -> intern_applied_reference intern env lvar args ref
             | CNotation (loc,ntn,([],[])) ->
                 let c = intern_notation intern env loc ntn ([],[]) in
-                find_appl_head_data lvar c, args
+                find_appl_head_data c, args
             | x -> (intern env f,[],[],[]), args in
 	let args =
 	  intern_impargs c env impargs args_scopes (merge_impargs l args) in
diff --git a/lib/util.ml b/lib/util.ml
index d71912289d..cdd3519301 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -853,6 +853,9 @@ let rec list_skipn n l = match n,l with
   | _, [] -> failwith "list_skipn"
   | n, _::l -> list_skipn (pred n) l
 
+let rec list_skipn_at_least n l =
+  try list_skipn n l with Failure _ -> []
+
 let rec list_addn n x l =
   if n = 0 then l else x :: (list_addn (pred n) x l)
 
diff --git a/lib/util.mli b/lib/util.mli
index 6ab9ce7c4b..7784635c3c 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -172,6 +172,7 @@ val list_firstn : int -> 'a list -> 'a list
 val list_last : 'a list -> 'a
 val list_lastn : int -> 'a list -> 'a list
 val list_skipn : int -> 'a list -> 'a list
+val list_skipn_at_least : int -> 'a list -> 'a list
 val list_addn : int -> 'a -> 'a list -> 'a list
 val list_prefix_of : 'a list -> 'a list -> bool
 (* [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *)