Imported Upstream version 8.3upstream/8.3

4 files changed, 22 insertions, 13 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b2b21925..fd230539 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: constrextern.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -602,7 +602,7 @@ let rec extern inctx scopes vars r =
     extern_symbol scopes vars r'' (uninterp_notations r'')
   with No_match -> match r' with
   | RRef (loc,ref) ->
-      extern_global loc (implicits_of_global ref)
+      extern_global loc (select_stronger_impargs (implicits_of_global ref))
         (extern_reference loc vars ref)
 
   | RVar (loc,id) -> CRef (Ident (loc,id))
@@ -655,7 +655,8 @@ let rec extern inctx scopes vars r =
 		 CRecord (loc, None, List.rev (ip projs locals args []))
 	       with
 		 | Not_found | No_match | Exit ->
-		     extern_app loc inctx (implicits_of_global ref)
+		     extern_app loc inctx
+		       (select_stronger_impargs (implicits_of_global ref))
 		       (Some ref,extern_reference rloc vars ref) args
 	     end
 	 | _       ->
@@ -828,12 +829,17 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 	      let subscopes =
 		try list_skipn n (find_arguments_scope ref) with _ -> [] in
 	      let impls =
-		try list_skipn n (implicits_of_global ref) with _ -> [] in
+		let impls =
+		  select_impargs_size
+		    (List.length args) (implicits_of_global ref) in
+		try list_skipn n impls 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
+	      let impls =
+		  select_impargs_size
+		    (List.length args) (implicits_of_global ref) in
 	      f, args, subscopes, impls
 	  | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], []
           | _, None -> t, [], [], []
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3bf556f1..d918e94d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: constrintern.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 open Pp
 open Util
@@ -41,7 +41,7 @@ type var_internalization_data =
        in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
     identifier list *
     (* signature of impargs of the variable *)
-    Impargs.implicits_list *
+    Impargs.implicit_status list *
     (* subscopes of the args of the variable *)
     scope_name option list
 
@@ -557,7 +557,7 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
-    RVar (loc,id), impls, argsc, expl_impls
+    RVar (loc,id), make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
   if Idset.mem id ids or List.mem id ltacvars
@@ -598,7 +598,7 @@ let find_appl_head_data = function
   | RApp (_,RRef (_,ref),l) as x
       when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
       let n = List.length l in
-      x,list_skipn_at_least n (implicits_of_global ref),
+      x,List.map (drop_first_implicits n) (implicits_of_global ref),
       list_skipn_at_least n (find_arguments_scope ref),[]
   | x -> x,[],[],[]
 
@@ -815,6 +815,7 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
 	  match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
       with Not_found ->
           anomaly "Inconsistent substitution of recursive notation")
+  | AHole _ -> ([],[[], PatVar (loc,Anonymous)])
   | t -> error_invalid_pattern_notation loc
   in aux alias fullsubst a
 
@@ -1372,6 +1373,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	    it_mkRLambda ibind body
 
   and intern_impargs c env l subscopes args =
+    let l = select_impargs_size (List.length args) l in
     let eargs, rargs = extract_explicit_arg l args in
     let rec aux n impl subscopes eargs rargs =
       let (enva,subscopes') = apply_scope_env env subscopes in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index acb13a8b..02a51e7e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: constrintern.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
+(*i $Id: constrintern.mli 13492 2010-10-04 21:20:01Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -53,7 +53,7 @@ type var_internalization_data =
     identifier list *
       (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
           in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
-    Impargs.implicits_list * (* signature of impargs of the variable *)
+    Impargs.implicit_status list * (** signature of impargs of the variable *)
     scope_name option list (* subscopes of the args of the variable *)
 
 (* A map of free variables to their implicit arguments and scopes *)
diff --git a/interp/notation.ml b/interp/notation.ml
index fe9d8b6d..8bf7ba21 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: notation.ml 13463 2010-09-24 22:21:29Z herbelin $ *)
 
 (*i*)
 open Util
@@ -113,7 +113,7 @@ let subst_scope (subst,sc) = sc
 
 open Libobject
 
-let discharge_scope (local,_,_ as o) =
+let discharge_scope (_,(local,_,_ as o)) =
   if local then None else Some o
 
 let classify_scope (local,_,_ as o) =
@@ -124,6 +124,7 @@ let (inScope,outScope) =
       cache_function = cache_scope;
       open_function = open_scope;
       subst_function = subst_scope;
+      discharge_function = discharge_scope;
       classify_function = classify_scope }
 
 let open_close_scope (local,opening,sc) =