Imported Upstream version 8.3.pl3upstream/8.3.pl3

26 files changed, 133 insertions, 95 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1716cfad..dc339622 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 13967 2011-04-08 14:08:43Z herbelin $ *)
+(* $Id: constrextern.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -729,13 +729,13 @@ let rec extern inctx scopes vars r =
 	     let listdecl =
 	       Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
-                 let (ids,bl) = extern_local_binder scopes vars bl in
+                 let (assums,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Idset.add) ids vars in
                  let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
 		 let n =
 		   match fst nv.(i) with
 		     | None -> None
-		     | Some x -> Some (dummy_loc, out_name (List.nth ids x))
+		     | Some x -> Some (dummy_loc, out_name (List.nth assums x))
 		 in
 		 let ro = extern_recursion_order scopes vars (snd nv.(i)) in
 		 ((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty,
@@ -745,7 +745,7 @@ let rec extern inctx scopes vars r =
 	 | RCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
-                 let (ids,bl) = extern_local_binder scopes vars blv.(i) in
+                 let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in
                  let vars0 = List.fold_right (name_fold Idset.add) ids vars in
                  let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
 		 ((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i),
@@ -795,24 +795,24 @@ and factorize_lambda inctx scopes vars aty c =
   | c -> ([],sub_extern inctx scopes vars c)
 
 and extern_local_binder scopes vars = function
-    [] -> ([],[])
+    [] -> ([],[],[])
   | (na,bk,Some bd,ty)::l ->
-      let (ids,l) =
+      let (assums,ids,l) =
         extern_local_binder scopes (name_fold Idset.add na vars) l in
-      (na::ids,
+      (assums,na::ids,
        LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
 
   | (na,bk,None,ty)::l ->
       let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
       (match extern_local_binder scopes (name_fold Idset.add na vars) l with
-          (ids,LocalRawAssum(nal,k,ty')::l)
+          (assums,ids,LocalRawAssum(nal,k,ty')::l)
             when same ty ty' &
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
-              (na::ids,
+              (na::assums,na::ids,
                LocalRawAssum((dummy_loc,na)::nal,k,ty')::l)
-        | (ids,l) ->
-            (na::ids,
+        | (assums,ids,l) ->
+            (na::assums,na::ids,
              LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l))
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
@@ -870,7 +870,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
                       termlists in
 		  let bll =
 		    List.map (fun (bl,(scopt,scl)) ->
-		      snd (extern_local_binder (scopt,scl@scopes') vars bl))
+		      pi3 (extern_local_binder (scopt,scl@scopes') vars bl))
                       binders in
 	          insert_delimiters (make_notation loc ntn (l,ll,bll)) key)
           | SynDefRule kn ->
@@ -1007,4 +1007,4 @@ let extern_constr_pattern env pat =
 let extern_rel_context where env sign =
   let a = detype_rel_context where [] (names_of_rel_context env) sign in
   let vars = vars_of_env env in
-  snd (extern_local_binder (None,[]) vars a)
+  pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 248abeda..d0ccde2a 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: constrextern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: constrextern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 524448a6..4310a01e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 13620 2010-11-04 14:11:49Z herbelin $ *)
+(* $Id: constrintern.ml 14656 2011-11-16 08:46:31Z herbelin $ *)
 
 open Pp
 open Util
@@ -322,6 +322,10 @@ let locate_if_isevar loc na = function
       with Not_found -> RHole (loc, Evd.BinderType na))
   | x -> x
 
+let reset_hidden_inductive_implicit_test (ltacvars,namedctxvars,ntnvars,impls) =
+  let f = function id,(Inductive _,b,c,d) -> id,(Inductive [],b,c,d) | x -> x in
+  (ltacvars,namedctxvars,ntnvars,List.map f impls)
+
 let check_hidden_implicit_parameters id (_,_,_,impls) =
   if List.exists (function
     | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams
@@ -461,6 +465,19 @@ let traverse_binder (terms,_,_ as subst)
     let renaming' = if id=id' then renaming else (id,id')::renaming in
     (renaming',env), Name id'
 
+let make_letins loc = List.fold_right (fun (na,b,t) c -> RLetIn (loc,na,b,c))
+
+let rec subordinate_letins letins = function
+  (* binders come in reverse order; the non-let are returned in reverse order together *)
+  (* with the subordinated let-in in writing order *)
+  | (na,_,Some b,t)::l ->
+      subordinate_letins ((na,b,t)::letins) l
+  | (na,bk,None,t)::l ->
+      let letins',rest = subordinate_letins [] l in
+      letins',((na,bk,t),letins)::rest
+  | [] ->
+      letins,[]
+
 let rec subst_iterator y t = function
   | RVar (_,id) as x -> if id = y then t else x
   | x -> map_rawconstr (subst_iterator y t) x
@@ -505,19 +522,21 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (bl,(scopt,subscopes)) = List.assoc x binders in
 	let env,bl = List.fold_left (iterate_binder intern lvar) (env,[]) bl in
+	let letins,bl = subordinate_letins [] bl in
         let termin = aux subst' (renaming,env) terminator in
-	List.fold_left (fun t binder ->
+	let res = List.fold_left (fun t binder ->
           subst_iterator ldots_var t
 	    (aux (terms,Some(x,binder)) subinfos iter))
-	  termin bl
+	  termin bl in
+	make_letins loc letins res
       with Not_found ->
           anomaly "Inconsistent substitution of recursive notation")
     | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt ->
-	let (na,bk,_,t) = snd (Option.get binderopt) in
-	RProd (loc,na,bk,t,aux subst' infos c')
+        let (na,bk,t),letins = snd (Option.get binderopt) in
+	RProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
     | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt ->
-	let (na,bk,_,t) = snd (Option.get binderopt) in
-	RLambda (loc,na,bk,t,aux subst' infos c')
+        let (na,bk,t),letins = snd (Option.get binderopt) in
+	RLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
     | t ->
       rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
 	(aux subst') subinfos t
@@ -846,7 +865,7 @@ let find_constructor ref f aliases pats scopes =
 	   if List.length pats < nvars then error_not_enough_arguments loc;
 	   let pats1,pats2 = list_chop nvars pats in
 	   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
-	   let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) scopes) args in
+	   let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) scopes) args in
 	   cstr, idspl1, pats2
        | _ -> raise Not_found)
 
@@ -1242,7 +1261,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
         let tms,env' = List.fold_right
           (fun citm (inds,env) ->
 	    let (tm,ind),nal = intern_case_item env citm in
-	    (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
+	    (tm,ind)::inds,List.fold_left
+              (push_name_env (reset_hidden_inductive_implicit_test lvar))
+              env nal)
 	  tms ([],env) in
         let rtnpo = Option.map (intern_type env') rtnpo in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
@@ -1251,7 +1272,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	let env' = reset_tmp_scope env in
         let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
         let p' = Option.map (fun p ->
-          let env'' = List.fold_left (push_name_env lvar) env ids in
+          let env'' = List.fold_left 
+            (push_name_env (reset_hidden_inductive_implicit_test lvar))
+            env ids in
 	  intern_type env'' p) po in
         RLetTuple (loc, List.map snd nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar) env nal) c)
@@ -1259,7 +1282,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
         let p' = Option.map (fun p ->
-          let env'' = List.fold_left (push_name_env lvar) env ids in
+          let env'' = List.fold_left
+            (push_name_env (reset_hidden_inductive_implicit_test lvar))
+            env ids in
 	  intern_type env'' p) po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole (loc, k) ->
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 02a51e7e..767ec9ff 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: constrintern.mli 13492 2010-10-04 21:20:01Z herbelin $ i*)
+(*i $Id: constrintern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 0848ccc7..c5850abf 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqlib.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: coqlib.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Pp
@@ -298,7 +298,7 @@ let build_coq_sumbool () = Lazy.force coq_sumbool
 
 (* Equality on Type as a Type *)
 let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity"
-let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity"
+let coq_identity_refl = lazy_init_constant ["Datatypes"] "identity_refl"
 let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
 let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
 let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 81cc3baa..64a9df6d 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqlib.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: coqlib.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 020c3622..c26133c6 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dumpglob.ml 13674 2010-12-04 10:34:11Z herbelin $ *)
+(* $Id: dumpglob.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 
 (* Dump of globalization (to be used by coqdoc) *)
@@ -110,9 +110,14 @@ let remove_sections dir =
     (* Theorem/Lemma outside its outer section of definition *)
     dir
 
+let interval loc =
+  let loc1,loc2 = Util.unloc loc in
+  loc1, loc2-1
+
 let dump_ref loc filepath modpath ident ty =
-  dump_string (Printf.sprintf "R%d %s %s %s %s\n"
-		  (fst (Util.unloc loc)) filepath modpath ident ty)
+  let bl,el = interval loc in
+  dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
+		  bl el filepath modpath ident ty)
 
 let add_glob_gen loc sp lib_dp ty =
   if dump () then
@@ -144,12 +149,14 @@ let add_glob_kn loc kn =
 let dump_binding loc id = ()
 
 let dump_definition (loc, id) sec s =
-  dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
+  let bl,el = interval loc in
+  dump_string (Printf.sprintf "%s %d:%d %s %s\n" s bl el
 			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
 
 let dump_reference loc modpath ident ty =
-  dump_string (Printf.sprintf "R%d %s %s %s %s\n"
-		  (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
+  let bl,el = interval loc in
+  dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
+		  bl el (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
 
 let dump_constraint ((loc, n), _, _) sec ty =
   match n with
@@ -167,18 +174,21 @@ let dump_modref loc mp ty =
     let l = if l = [] then l else Util.list_drop_last l in
     let fp = Names.string_of_dirpath dp in
     let mp = Names.string_of_dirpath (Names.make_dirpath l) in
-      dump_string (Printf.sprintf "R%d %s %s %s %s\n"
-		      (fst (Util.unloc loc)) fp mp "<>" ty)
+    let bl,el = interval loc in
+      dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
+		      bl el fp mp "<>" ty)
 
 let dump_moddef loc mp ty =
   if dump () then
+    let bl,el = interval loc in
     let (dp, l) = Lib.split_modpath mp in
     let mp = Names.string_of_dirpath (Names.make_dirpath l) in
-      dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
+      dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el "<>" mp)
 
 let dump_libref loc dp ty =
-  dump_string (Printf.sprintf "R%d %s <> <> %s\n"
-		  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
+  let bl,el = interval loc in
+  dump_string (Printf.sprintf "R%d:%d %s <> <> %s\n"
+		  bl el (Names.string_of_dirpath dp) ty)
 
 let cook_notation df sc =
   (* We encode notations so that they are space-free and still human-readable *)
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 049bad5a..d3215c7d 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dumpglob.mli 13328 2010-07-26 11:05:30Z herbelin $ *)
+(* $Id: dumpglob.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 
 val open_glob_file : string -> unit
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 310420aa..dd75bbfc 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: genarg.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: genarg.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 9c9096bb..54b415d1 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: genarg.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: genarg.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Util
 open Names
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 22075654..88ed0873 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: implicit_quantifiers.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: implicit_quantifiers.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index b8f6594a..4442e09d 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: implicit_quantifiers.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: implicit_quantifiers.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/interp/modintern.ml b/interp/modintern.ml
index bed5597e..f53d1796 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: modintern.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: modintern.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 1cf8a5bd..e3a7cc6a 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modintern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: modintern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Declarations
diff --git a/interp/notation.ml b/interp/notation.ml
index 8bf7ba21..6e02c40b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 13463 2010-09-24 22:21:29Z herbelin $ *)
+(* $Id: notation.ml 14820 2011-12-18 22:11:32Z herbelin $ *)
 
 (*i*)
 open Util
@@ -328,17 +328,18 @@ let declare_uninterpretation rule (metas,c as pat) =
   let (key,n) = aconstr_key c in
   notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
 
-let rec find_interpretation find = function
+let rec find_interpretation ntn find = function
   | [] -> raise Not_found
-  | sce :: scopes ->
-      let sc,sco = match sce with
-	| Scope sc -> sc, Some sc
-	| SingleNotation _ -> default_scope, None in
-      try
-	let (pat,df) = find sc in
-	pat,(df,sco)
-      with Not_found ->
-	find_interpretation find scopes
+  | Scope scope :: scopes ->
+      (try let (pat,df) = find scope in pat,(df,Some scope)
+       with Not_found -> find_interpretation ntn find scopes)
+  | SingleNotation ntn'::scopes when ntn' = ntn ->
+      (try let (pat,df) = find default_scope in pat,(df,None)
+       with Not_found ->
+         (* e.g. because single notation only for constr, not cases_pattern *)
+         find_interpretation ntn find scopes)
+  | SingleNotation _::scopes ->
+      find_interpretation ntn find scopes
 
 let find_notation ntn sc =
   Gmap.find ntn (find_scope sc).notations
@@ -361,7 +362,8 @@ let find_prim_token g loc p sc =
 
 let interp_prim_token_gen g loc p local_scopes =
   let scopes = make_current_scopes local_scopes in
-  try find_interpretation (find_prim_token g loc p) scopes
+  let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
+  try find_interpretation p_as_ntn (find_prim_token g loc p) scopes
   with Not_found ->
     user_err_loc (loc,"interp_prim_token",
     (match p with
@@ -376,7 +378,7 @@ let interp_prim_token_cases_pattern loc p name =
 
 let rec interp_notation loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
-  try find_interpretation (find_notation ntn) scopes
+  try find_interpretation ntn (find_notation ntn) scopes
   with Not_found ->
     user_err_loc
     (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
diff --git a/interp/notation.mli b/interp/notation.mli
index 72b576eb..33ffe7b4 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: notation.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: notation.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 618f8320..71029f3f 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ppextend.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(*i $Id: ppextend.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (*i*)
 open Pp
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 6c386162..e2c4ca98 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ppextend.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
+(*i $Id: ppextend.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 2225bb6e..b0303a30 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reserve.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: reserve.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* Reserved names *)
 
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 613ba830..fb60c038 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reserve.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: reserve.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Util
 open Names
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 56a29c73..3eb7c248 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 5ca4e853..720c88bb 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 77b34d4f..44bb02ad 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: syntax_def.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: syntax_def.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 33d4c5d3..a3f846bb 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: syntax_def.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: syntax_def.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a358249f..2d4e41ec 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml 13680 2010-12-04 15:06:06Z herbelin $ *)
+(* $Id: topconstr.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -722,6 +722,7 @@ let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with
       match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
   | RCast(_,c1, CastCoerce), ACast(c2, CastCoerce) ->
       match_ alp metas sigma c1 c2
+  | RSort (_,RType _), ASort (RType None) -> sigma
   | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
   | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, AHole _ -> sigma
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 5e49d2ea..ce9de27b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: topconstr.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: topconstr.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Pp