Merge branch 'v8.5' into trunk

36 files changed, 275 insertions, 155 deletions

diff --git a/CHANGES b/CHANGES
index 7f1f8b9699..49b4830c4b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -53,6 +53,11 @@ API
 Tools
 
 - Added an option -w to control the output of coqtop warnings.
+- Configure now takes an optional -native-compiler (yes|no) flag replacing
+  -no-native-compiler. The new flag is set to no by default under Windows.
+- Flag -no-native-compiler was removed and became the default for coqc. If
+  precompilation of files for native conversion test is desired, use
+  -native-compiler.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
diff --git a/configure.ml b/configure.ml
index ffb7c15f5e..7e0d68eb89 100644
--- a/configure.ml
+++ b/configure.ml
@@ -252,7 +252,7 @@ module Prefs = struct
   let profile = ref false
   let annotate = ref false
   let makecmd = ref "make"
-  let nativecompiler = ref true
+  let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
   let coqwebsite = ref "http://coq.inria.fr/"
   let force_caml_version = ref false
 end
@@ -331,8 +331,8 @@ let args_options = Arg.align [
     " Dumps ml annotation files while compiling Coq";
   "-makecmd", Arg.Set_string Prefs.makecmd,
     "<command> Name of GNU Make command";
-  "-no-native-compiler", Arg.Clear Prefs.nativecompiler,
-    " No compilation to native code for conversion and normalization";
+  "-native-compiler", arg_bool Prefs.nativecompiler,
+    " (yes|no) Compilation to native code for conversion and normalization";
   "-coqwebsite", Arg.Set_string Prefs.coqwebsite,
     " URL of the coq website";
   "-force-caml-version", arg_bool Prefs.force_caml_version,
diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
index 5b421e49dd..676490510c 100755
--- a/dev/nsis/coq.nsi
+++ b/dev/nsis/coq.nsi
@@ -95,8 +95,8 @@ Section "Coq" Sec1
   File /r ${COQ_SRC_PATH}\theories\*.vo
   File /r ${COQ_SRC_PATH}\theories\*.v
   File /r ${COQ_SRC_PATH}\theories\*.glob
-  File /r ${COQ_SRC_PATH}\theories\*.cmi
-  File /r ${COQ_SRC_PATH}\theories\*.cmxs
+  ; File /r ${COQ_SRC_PATH}\theories\*.cmi
+  ; File /r ${COQ_SRC_PATH}\theories\*.cmxs
   SetOutPath "$INSTDIR\lib\plugins"
   File /r ${COQ_SRC_PATH}\plugins\*.vo
   File /r ${COQ_SRC_PATH}\plugins\*.v
diff --git a/engine/evd.ml b/engine/evd.ml
index 168a10df93..fc4f5e040e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -277,15 +277,15 @@ end
 type evar_universe_context = 
  { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
    uctx_local : Univ.universe_context_set; (** The local context of variables *)
-    uctx_univ_variables : Universes.universe_opt_subst;
-      (** The local universes that are unification variables *)
-    uctx_univ_algebraic : Univ.universe_set; 
-    (** The subset of unification variables that
+   uctx_univ_variables : Universes.universe_opt_subst;
+   (** The local universes that are unification variables *)
+   uctx_univ_algebraic : Univ.universe_set; 
+   (** The subset of unification variables that
 	can be instantiated with algebraic universes as they appear in types 
 	and universe instances only. *)
-    uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
-    uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
-  }
+   uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
+   uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
+ }
   
 let empty_evar_universe_context = 
   { uctx_names = UNameMap.empty, Univ.LMap.empty;
@@ -769,10 +769,10 @@ let empty = {
   extras = Store.empty;
 }
 
-let from_env ?ctx e = 
-  match ctx with
-  | None -> { empty with universes = evar_universe_context_from e }
-  | Some ctx -> { empty with universes = ctx }
+let from_env e = 
+  { empty with universes = evar_universe_context_from e }
+
+let from_ctx ctx = { empty with universes = ctx }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
@@ -982,9 +982,43 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = d.universes.uctx_local
 
-let universe_context evd =
-  Univ.ContextSet.to_context evd.universes.uctx_local
+let pr_uctx_level uctx = 
+  let map, map_rev = uctx.uctx_names in 
+    fun l ->
+      try str(Univ.LMap.find l map_rev)
+      with Not_found -> 
+	Universes.pr_with_global_universes l
 
+let universe_context ?names evd =
+  match names with
+  | None -> Univ.ContextSet.to_context evd.universes.uctx_local
+  | Some pl ->
+     let levels = Univ.ContextSet.levels evd.universes.uctx_local in
+     let newinst, left =
+       List.fold_right
+         (fun (loc,id) (newinst, acc) ->
+	  let l =
+	    try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names)
+	    with Not_found ->
+	      user_err_loc (loc, "universe_context",
+			    str"Universe " ++ pr_id id ++ str" is not bound anymore.")
+	  in (l :: newinst, Univ.LSet.remove l acc))
+	 pl ([], levels)
+     in
+       if not (Univ.LSet.is_empty left) then
+         let n = Univ.LSet.cardinal left in
+           errorlabstrm "universe_context"
+			(str(CString.plural n "Universe") ++ spc () ++
+			     Univ.LSet.pr (pr_uctx_level evd.universes) left ++
+			     spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")
+       else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst),
+				Univ.ContextSet.constraints evd.universes.uctx_local)
+
+let restrict_universe_context evd vars =
+  let uctx = evd.universes in
+  let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in
+    { evd with universes = { uctx with uctx_local = uctx' } }
+						 
 let universe_subst evd =
   evd.universes.uctx_univ_variables
 
@@ -1072,6 +1106,15 @@ let make_flexible_variable evd b u =
     {evd with universes = {ctx with uctx_univ_variables = uvars'; 
       uctx_univ_algebraic = avars'}}
 
+let make_evar_universe_context e l = 
+  let uctx = evar_universe_context_from e in
+    match l with
+    | None -> uctx
+    | Some us ->
+       List.fold_left (fun uctx (loc,id) ->
+		       fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) uctx))
+		      uctx us
+    
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
@@ -1703,13 +1746,6 @@ let evar_dependency_closure n sigma =
 let has_no_evar sigma =
   EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
 
-let pr_uctx_level uctx = 
-  let map, map_rev = uctx.uctx_names in 
-    fun l ->
-      try str(Univ.LMap.find l map_rev)
-      with Not_found -> 
-	Universes.pr_with_global_universes l
-
 let pr_evd_level evd = pr_uctx_level evd.universes
 
 let pr_evar_universe_context ctx =
diff --git a/engine/evd.mli b/engine/evd.mli
index f2d8a83350..94d9d5f662 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -129,10 +129,13 @@ type evar_map
 val empty : evar_map
 (** The empty evar map. *)
 
-val from_env : ?ctx:evar_universe_context -> env -> evar_map
+val from_env : env -> evar_map
 (** The empty evar map with given universe context, taking its initial 
     universes from env. *)
 
+val from_ctx : evar_universe_context -> evar_map
+(** The empty evar map with given universe context *)
+
 val is_empty : evar_map -> bool
 (** Whether an evarmap is empty. *)
 
@@ -484,6 +487,8 @@ val union_evar_universe_context : evar_universe_context -> evar_universe_context
   evar_universe_context
 val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
 
+val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context
+val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map							   
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> string -> Univ.universe_level
 val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
@@ -527,7 +532,7 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
 
 val evar_universe_context : evar_map -> evar_universe_context
 val universe_context_set : evar_map -> Univ.universe_context_set
-val universe_context : evar_map -> Univ.universe_context
+val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> Univ.universes
 
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 2cffdf816e..e97a2eceef 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -201,7 +201,7 @@ object(self)
     let on_changed (i, f) = segment#add i (flags_to_color f) in
     let on_push s =
       set_index s document_length;
-      (SentenceId.connect s)#changed on_changed;
+      ignore ((SentenceId.connect s)#changed on_changed);
       document_length <- succ document_length;
       segment#set_length document_length;
       let flags = List.map mem_flag_of_flag s.flags in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ecaf2b8c13..c754f1910c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1142,7 +1142,11 @@ let drop_notations_pattern looked_for =
 	sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
       begin match sorted_fields with
 	| None -> RCPatAtom (loc, None)
-	| Some (_, head, pl) ->
+	| Some (n, head, pl) ->
+          let pl =
+            if !oldfashion_patterns then pl else
+            let pars = List.make n (CPatAtom (loc, None)) in
+            List.rev_append pars pl in
 	  match drop_syndef top env head pl with
 	    |Some (a,b,c) -> RCPatCstr(loc, a, b, c)
 	    |None -> raise (InternalizationError (loc,NotAConstructor head))
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index bb0331fcc4..37218fbf91 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -160,6 +160,9 @@ type option_ref_value =
   | StringRefValue of string
   | QualidRefValue of reference
 
+(** Identifier and optional list of bound universes. *)						 
+type plident = lident * lident list option
+
 type sort_expr = glob_sort
 
 type definition_expr =
@@ -168,10 +171,10 @@ type definition_expr =
       * constr_expr option
 
 type fixpoint_expr =
-    Id.t located * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
+    plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
 
 type cofixpoint_expr =
-    Id.t located * local_binder list * constr_expr * constr_expr option
+    plident * local_binder list * constr_expr * constr_expr option
 
 type local_decl_expr =
   | AssumExpr of lname * constr_expr
@@ -190,14 +193,14 @@ type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
   | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
 type inductive_expr =
-  lident with_coercion * local_binder list * constr_expr option * inductive_kind *
+  plident with_coercion * local_binder list * constr_expr option * inductive_kind *
     constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
-  lident * local_binder list * constr_expr option * constructor_expr list
+  plident * local_binder list * constr_expr option * constructor_expr list
 
 type proof_expr =
-  lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)
+  plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)
 
 type grammar_tactic_prod_item_expr =
   | TacTerm of string
@@ -305,7 +308,7 @@ type vernac_expr =
 
   (* Gallina *)
   | VernacDefinition of
-      (locality option * definition_object_kind) * lident * definition_expr
+      (locality option * definition_object_kind) * plident * definition_expr
   | VernacStartTheoremProof of theorem_kind * proof_expr list * bool
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 11f78c708c..63850713f2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -196,9 +196,9 @@ GEXTEND Gram
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr;
+    [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
         l = LIST0
-          [ "with"; id = identref; bl = binders; ":"; c = lconstr ->
+          [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
           (Some id,(bl,c,None)) ] ->
           VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
       | stre = assumption_token; nl = inline; bl = assum_list ->
@@ -206,10 +206,10 @@ GEXTEND Gram
       | stre = assumptions_token; nl = inline; bl = assum_list ->
 	  test_plurial_form bl;
 	  VernacAssumption (stre, nl, bl)
-      | d = def_token; id = identref; b = def_body ->
+      | d = def_token; id = pidentref; b = def_body ->
           VernacDefinition (d, id, b)
       | IDENT "Let"; id = identref; b = def_body ->
-          VernacDefinition ((Some Discharge, Definition), id, b)
+          VernacDefinition ((Some Discharge, Definition), (id, None), b)
       (* Gallina inductive declarations *)
       | priv = private_token; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
@@ -268,6 +268,9 @@ GEXTEND Gram
       | IDENT "Inline" -> DefaultInline
       | -> NoInline] ]
   ;
+  pidentref:
+    [ [ i = identref; l = OPT [ "@{" ; l = LIST1 identref; "}" -> l ] -> (i,l) ] ]
+  ;
   univ_constraint:
     [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
 	r = identref -> (l, ord, r) ] ]
@@ -312,7 +315,7 @@ GEXTEND Gram
       | -> RecordDecl (None, []) ] ]
   ;
   inductive_definition:
-    [ [ oc = opt_coercion; id = identref; indpar = binders;
+    [ [ oc = opt_coercion; id = pidentref; indpar = binders;
         c = OPT [ ":"; c = lconstr -> c ];
         lc=opt_constructors_or_fields; ntn = decl_notation ->
 	   (((oc,id),indpar,c,lc),ntn) ] ]
@@ -338,14 +341,14 @@ GEXTEND Gram
   ;
   (* (co)-fixpoints *)
   rec_definition:
-    [ [ id = identref;
+    [ [ id = pidentref;
 	bl = binders_fixannot;
         ty = type_cstr;
 	def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
 	  let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = identref; bl = binders; ty = type_cstr;
+    [ [ id = pidentref; bl = binders; ty = type_cstr;
         def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
@@ -605,15 +608,15 @@ GEXTEND Gram
           d = def_body ->
           let s = coerce_reference_to_id qid in
 	  VernacDefinition
-	    ((Some Global,CanonicalStructure),(Loc.ghost,s),d)
+	    ((Some Global,CanonicalStructure),((Loc.ghost,s),None),d)
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-	  VernacDefinition ((None,Coercion),(Loc.ghost,s),d)
+	  VernacDefinition ((None,Coercion),((Loc.ghost,s),None),d)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = coerce_reference_to_id qid in
-	  VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d)
+	  VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.ghost,s),None),d)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
 	   VernacIdentityCoercion (true, f, s, t)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 065c12a2d7..07efaae27b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1395,7 +1395,7 @@ let do_build_inductive
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors =
-    ((Loc.ghost,relnames.(i)),
+    (((Loc.ghost,relnames.(i)), None),
     rel_params,
     Some rel_arities.(i),
     ext_rel_constructors),[]
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 5dcb0c0439..d9d059f8fa 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -150,7 +150,7 @@ let build_newrecursive
   in
   let (rec_sign,rec_impls) =
     List.fold_left
-      (fun (env,impls) ((_,recname),bl,arityc,_) ->
+      (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
         let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
 	let evdref =  ref (Evd.from_env env0) in
@@ -323,7 +323,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
     is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
     (continue_proof : int -> Names.constant array -> Term.constr array -> int ->
       Tacmach.tactic) : unit =
-  let names = List.map (function ((_, name),_,_,_,_),_ -> name) fix_rec_l in
+  let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
   let funs_types =  List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
@@ -343,7 +343,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 		 locate_ind
 		 f_R_mut)
 	in
-	let fname_kn ((fname,_,_,_,_),_) =
+	let fname_kn (((fname,_),_,_,_,_),_) =
 	  let f_ref = Ident fname in
 	  locate_with_msg
 	    (pr_reference f_ref++str ": Not an inductive type!")
@@ -380,15 +380,15 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
   match fixpoint_exprl with
-    | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
+    | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
       Command.do_definition
 	fname
-	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition)
+	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
        let evd,rev_pconstants =
 	 List.fold_left
-	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+	   (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -402,7 +402,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
-	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
+	   (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -614,7 +614,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
   let _is_struct =
     match fixpoint_exprl with
       | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
- 	  let ((((_,name),_,args,types,body)),_)  as fixpoint_expr =
+ 	  let (((((_,name),pl),_,args,types,body)),_)  as fixpoint_expr =
 	    match recompute_binder_list [fixpoint_expr] with 
 	      | [e] -> e
 	      | _ -> assert false
@@ -638,7 +638,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	  then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook;
 	  false
       |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
- 	  let ((((_,name),_,args,types,body)),_)  as fixpoint_expr =
+ 	  let (((((_,name),_),_,args,types,body)),_)  as fixpoint_expr =
 	    match recompute_binder_list [fixpoint_expr] with 
 	      | [e] -> e
 	      | _ -> assert false
@@ -672,7 +672,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	    fixpoint_exprl;
 	let fixpoint_exprl = recompute_binder_list fixpoint_exprl in 
 	let fix_names =
-	  List.map (function (((_,name),_,_,_,_),_) -> name) fixpoint_exprl
+	  List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl
 	in
 	(* ok all the expressions are structural *)
   	let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
@@ -867,20 +867,20 @@ let make_graph (f_ref:global_reference) =
 			    )
 			in
 			let b' = add_args (snd id) new_args b in
-			(((id, ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+			((((id,None), ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
 		     )
 		     fixexprl
 		 in
 		 l
 	     | _ ->
 		let id = Label.to_id (con_label c) in
-		 [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+		 [(((Loc.ghost,id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
 	 let mp,dp,_ = repr_con c in
 	 do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list;
 	 (* We register the infos *)
 	 List.iter
-	   (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
+	   (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
 	   expr_list);
   Dumpglob.continue ()
 
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ea699580b9..69e055c23b 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -841,7 +841,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     FIXME: params et cstr_expr (arity) *)
 let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
     (rawlist:(Id.t * glob_constr) list) =
-  let lident = Loc.ghost, shift.ident in
+  let lident = (Loc.ghost, shift.ident), None in
   let bindlist , cstr_expr = (* params , arities *)
     merge_rec_params_and_arity prms1 prms2 shift mkSet in
   let lcstor_expr : (bool * (lident * constr_expr)) list  =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b5a42b3078..9c09a4a0cc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1398,9 +1398,7 @@ let com_terminate
   start_proof ctx tclIDTAC tclIDTAC;
   try
     let sigma, new_goal_type = build_new_goal_type () in
-    let sigma =
-      Evd.from_env ~ctx:(Evd.evar_universe_context sigma) Environ.empty_env
-    in
+    let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in
     open_new_goal start_proof sigma
       using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
@@ -1437,9 +1435,7 @@ let (com_eqn : int -> Id.t ->
 	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
     in
     let (evmap, env) = Lemmas.get_current_context() in
-    let evmap =
-      Evd.from_env ~ctx:(Evd.evar_universe_context evmap) Environ.empty_env
-    in
+    let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4e889e55f0..71dcd15cc7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -43,6 +43,12 @@ module Make
     else
       pr_id id
 
+  let pr_plident (lid, l) =
+    pr_lident lid ++
+    (match l with
+     | Some l -> prlist_with_sep spc pr_lident l
+     | None -> mt())
+    
   let string_of_fqid fqid =
     String.concat "." (List.map Id.to_string fqid)
 
@@ -387,10 +393,16 @@ module Make
              hov 0 (prlist_with_sep sep pr_production_item pil ++
                       spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
 
-  let pr_statement head (id,(bl,c,guard)) =
-    assert (not (Option.is_empty id));
+  let pr_univs pl =
+    match pl with
+    | None -> mt ()
+    | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
+
+  let pr_statement head (idpl,(bl,c,guard)) =
+    assert (not (Option.is_empty idpl));
+    let id, pl = Option.get idpl in
     hov 2
-      (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
+      (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
          (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
          pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
          str":" ++ pr_spc_lconstr c)
@@ -729,7 +741,7 @@ module Make
           return (
             hov 2 (
               pr_def_token d ++ spc()
-              ++ pr_lident id ++ binds ++ typ
+              ++ pr_plident id ++ binds ++ typ
               ++ (match c with
                 | None -> mt()
                 | Some cc -> str" :=" ++ spc() ++ cc))
@@ -781,10 +793,10 @@ module Make
             | RecordDecl (c,fs) ->
               pr_record_decl b c fs
           in
-          let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+          let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) =
             hov 0 (
               str key ++ spc() ++
-                (if coe then str"> " else str"") ++ pr_lident id ++
+                (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++
                 pr_and_type_binders_arg indpar ++ spc() ++
                 Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
                 str" :=") ++ pr_constructor_list k lc ++
@@ -808,9 +820,9 @@ module Make
             | None | Some Global -> ""
           in
           let pr_onerec = function
-            | ((loc,id),ro,bl,type_,def),ntn ->
+            | (((loc,id),pl),ro,bl,type_,def),ntn ->
               let annot = pr_guard_annot pr_lconstr_expr bl ro in
-              pr_id id ++ pr_binders_arg bl ++ annot
+              pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
               ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
               ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
                 prlist (pr_decl_notation pr_constr) ntn
@@ -826,8 +838,8 @@ module Make
             | Some Local -> keyword "Local" ++ spc ()
             | None | Some Global -> str ""
           in
-          let pr_onecorec (((loc,id),bl,c,def),ntn) =
-            pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+          let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) =
+            pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
               spc() ++ pr_lconstr_expr c ++
               pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
               prlist (pr_decl_notation pr_constr) ntn
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e48a336a6e..3363d0300d 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -133,7 +133,7 @@ open Decl_kinds
 let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
-  let evd = Evd.from_env ~ctx Environ.empty_env in
+  let evd = Evd.from_env ~ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
   start_proof id goal_kind evd sign typ terminator;
   try
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index df10e7376a..934642f123 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -212,7 +212,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
 let default_thm_id = Id.of_string "Unnamed_thm"
 
 let compute_proof_name locality = function
-  | Some (loc,id) ->
+  | Some ((loc,id),pl) ->
       (* We check existence here: it's a bit late at Qed time *)
       if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
 	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
@@ -439,7 +439,11 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
 
 let start_proof_com kind thms hook =
   let env0 = Global.env () in
-  let evdref = ref (Evd.from_env env0) in
+  let levels = Option.map snd (fst (List.hd thms)) in 
+  let evdref = ref (match levels with
+		    | None -> Evd.from_env env0
+		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
+  in
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
diff --git a/stm/stm.ml b/stm/stm.ml
index e6271f6089..4a303f036e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -424,8 +424,8 @@ end = struct (* {{{ *)
   let reachable id = reachable !vcs id
   let mk_branch_name { expr = x } = Branch.make
     (match x with
-    | VernacDefinition (_,(_,i),_) -> string_of_id i
-    | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id i
+    | VernacDefinition (_,((_,i),_),_) -> string_of_id i
+    | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i
     | _ -> "branch")
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index aaa6c2c07d..fb41bb7bea 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -244,7 +244,7 @@ and pp_local_decl_expr lde = (* don't know what it is for now *)
   match lde with
   | AssumExpr (_, ce) -> pp_expr ce
   | DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, (l, id)), lbl, ceo, _, cl_or_rdexpr) =
+and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
   (* inductive_expr *)
   let b,e = Loc.unloc l in
   let location = ["begin", string_of_int b; "end", string_of_int e] in
@@ -273,7 +273,7 @@ and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
     | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
     | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
   Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
+and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
   (* fixpoint_expr *)
   let start, stop = unlock loc in
   let id = Id.to_string id in
@@ -286,7 +286,7 @@ and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
   | Some ce -> [pp_expr ce]
   | None -> []
   end
-and pp_cofixpoint_expr ((loc, id), lbl, ce, ceo) = (* cofixpoint_expr *)
+and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
   (* Nota: it is like fixpoint_expr without (optid, roe)
    * so could be merged if there is no more differences *)
   let start, stop = unlock loc in
@@ -473,7 +473,7 @@ and pp_expr ?(attr=[]) e =
       xmlApply loc
         (xmlOperator "fix" loc ::
            List.flatten (List.map
-             (fun (a,b,cl,c,d) -> pp_fixpoint_expr (a,b,cl,c,Some d))
+             (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
              fel))
 
 let pp_comment (c) =
@@ -540,7 +540,7 @@ let rec tmpp v loc =
   | VernacConstraint _
   | VernacPolymorphic (_, _) as x -> xmlTODO loc x
   (* Gallina *)
-  | VernacDefinition (ldk, (_,id), de) ->
+  | VernacDefinition (ldk, ((_,id),_), de) ->
       let l, dk =
         match ldk with
         | Some l, dk -> (l, dk)
@@ -555,7 +555,7 @@ let rec tmpp v loc =
       let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
       let str_id = Id.to_string id in
       (xmlDef str_dk str_id loc [pp_expr e])
-  | VernacStartTheoremProof (tk, [ Some (_,id), ([], statement, None) ], b) ->
+  | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
       let str_tk = Kindops.string_of_theorem_kind tk in
       let str_id = Id.to_string id in
       (xmlThm str_tk str_id loc [pp_expr statement])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2b5eb86834..8aa2a59177 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -116,25 +116,25 @@ let rec classify_vernac e =
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
     | VernacDefinition (
-       (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) ->
+       (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
         VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
-    | VernacDefinition (_,(_,i),ProveBody _) ->
+    | VernacDefinition (_,((_,i),_),ProveBody _) ->
         VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
     | VernacStartTheoremProof (_,l,_) ->
         let ids = 
-          CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
+          CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
         VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
     | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
     | VernacFixpoint (_,l) ->
         let ids, open_proof =
-          List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
+          List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
         then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (_,l) ->
         let ids, open_proof =
-          List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
+          List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
         then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
@@ -143,9 +143,9 @@ let rec classify_vernac e =
     | VernacAssumption (_,_,l) ->
         let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
         VtSideff ids, VtLater    
-    | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
+    | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
     | VernacInductive (_,_,l) ->
-        let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
+        let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
            CList.map_filter (function
@@ -173,9 +173,13 @@ let rec classify_vernac e =
     | VernacDeclareReduction _
     | VernacDeclareClass _ | VernacDeclareInstances _
     | VernacRegister _
-    | VernacDeclareTacticDefinition _
     | VernacNameSectionHypSet _
     | VernacComments _ -> VtSideff [], VtLater
+    | VernacDeclareTacticDefinition (_,l) ->
+        let open Libnames in
+        VtSideff (List.map (function
+          | (Ident (_,r),_,_) -> r
+          | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
     (* (Local) Notations have to disappear *)
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 749e0d2b5b..e1c9c2de59 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -51,7 +51,7 @@ let optimize_non_type_induction_scheme kind dep sort ind =
     let u = Univ.UContext.instance ctx in
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
-    let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
+    let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
       (c, Evd.evar_universe_context sigma), Declareops.no_seff
 
 let build_induction_scheme_in_type dep sort ind =
@@ -63,7 +63,7 @@ let build_induction_scheme_in_type dep sort ind =
   let u = Univ.UContext.instance ctx in
   let ctxset = Univ.ContextSet.of_context ctx in
   let ectx = Evd.evar_universe_context_of ctxset in
-  let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
+  let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
     c, Evd.evar_universe_context sigma
  
 let rect_scheme_kind_from_type =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9a64b03fd1..efd6ded44c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     errorlabstrm "lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
-  let pf = Proof.start (Evd.from_env ~ctx:(evar_universe_context sigma) invEnv) [invEnv,invGoal] in
+  let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
       tclTHEN intro (onLastHypId inv_op)) pf)
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 719cc7c98d..aa057a3e86 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1824,8 +1824,8 @@ let declare_projection n instance_id r =
 
 let build_morphism_signature m =
   let env = Global.env () in
-  let m,ctx = Constrintern.interp_constr env Evd.empty m in
-  let sigma = Evd.from_env ~ctx env in
+  let m,ctx = Constrintern.interp_constr env (Evd.from_env env) m in
+  let sigma = Evd.from_ctx ctx in
   let t = Typing.unsafe_type_of env sigma m in
   let cstrs =
     let rec aux t =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4c53d5340b..fea7ab72e4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2222,6 +2222,11 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
   | IntroApplyOn (f,(loc,pat)) ->
       let naming,tac_ipat =
         prepare_intros_loc loc (IntroIdentifier id) destopt pat in
+      let doclear =
+        if naming = NamingMustBe (loc,id) then
+          Proofview.tclUNIT () (* apply_in_once do a replacement *)
+        else
+          Proofview.V82.tactic (clear [id]) in
       Proofview.Goal.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
@@ -2230,7 +2235,9 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
              (apply_in_once false true true true naming id
-                (None,(sigma,(c,NoBindings))) tac_ipat) (tac ((dloc,id)::thin) None []))
+                (None,(sigma,(c,NoBindings)))
+                (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id)))
+             (tac thin None []))
           sigma
       end
 
@@ -2296,7 +2303,9 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
     apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
       naming id lemma tac in
   Proofview.Goal.enter begin fun gl ->
-  let destopt = get_previous_hyp_position id gl in
+  let destopt =
+    if with_evars then MoveLast (* evars would depend on the whole context *)
+    else get_previous_hyp_position id gl in
   let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in
   let lemmas_target, last_lemma_target =
     let last,first = List.sep_last lemmas in
diff --git a/test-suite/bugs/closed/4316.v b/test-suite/bugs/closed/4316.v
new file mode 100644
index 0000000000..68dec1334a
--- /dev/null
+++ b/test-suite/bugs/closed/4316.v
@@ -0,0 +1,3 @@
+Ltac tac := idtac.
+Reset tac.
+Ltac tac := idtac.
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 23f33081b4..66458543aa 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -16,3 +16,5 @@ extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
 Closed under the global context
 Closed under the global context
+Axioms:
+M.foo : False
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index f23bc49808..c2003816ca 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -94,3 +94,19 @@ Proof (false_positive.add_comm 5).
 
 Print Assumptions comm_plus5.
 (* Should answer : Closed under the global context *)
+
+(** Print Assumption and Include *)
+
+Module INCLUDE.
+
+Module M.
+Axiom foo : False.
+End M.
+
+Module N.
+Include M.
+End N.
+
+Print Assumptions N.foo.
+
+End INCLUDE.
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index ae1694c58c..35ba94fb67 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -61,3 +61,11 @@ Goal forall n, n = S n -> 0=0.
 intros n H/n_Sn.
 destruct H.
 Qed.
+
+(* Another check about generated names and cleared hypotheses with
+   pat/c patterns *)
+Goal (True -> 0=0 /\ 1=1) -> True -> 0=0.
+intros H (H1,?)/H.
+change (1=1) in H0.
+exact H1.
+Qed.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b21845aea6..e0475646fa 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -770,7 +770,7 @@ let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l
 	&& not_tops mllib && not_tops mlpack) then
     l
   else
-    ((".",here)::ml_inc,(".","Top",here)::i_inc,r_inc)
+    ((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc)
 
 let warn_install_at_root_directory
     (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) =
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index a11653a43b..4d8ba0f789 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -171,28 +171,28 @@ let rec traverse current ctx accu t = match kind_of_term t with
 
 and traverse_object ?inhabits (curr, data, ax2ty) body obj =
   let data, ax2ty =
-    let already_in = Refmap.mem obj data in
+    let already_in = Refmap_env.mem obj data in
     match body () with
     | None ->
         let data =
-          if not already_in then Refmap.add obj Refset.empty data else data in
+          if not already_in then Refmap_env.add obj Refset_env.empty data else data in
         let ax2ty =
           if Option.is_empty inhabits then ax2ty else
           let ty = Option.get inhabits in
-          try let l = Refmap.find obj ax2ty in Refmap.add obj (ty::l) ax2ty 
-          with Not_found -> Refmap.add obj [ty] ax2ty in
+          try let l = Refmap_env.find obj ax2ty in Refmap_env.add obj (ty::l) ax2ty 
+          with Not_found -> Refmap_env.add obj [ty] ax2ty in
         data, ax2ty
     | Some body ->
       if already_in then data, ax2ty else
       let contents,data,ax2ty =
-        traverse (label_of obj) [] (Refset.empty,data,ax2ty) body in
-      Refmap.add obj contents data, ax2ty
+        traverse (label_of obj) [] (Refset_env.empty,data,ax2ty) body in
+      Refmap_env.add obj contents data, ax2ty
   in
-  (Refset.add obj curr, data, ax2ty)
+  (Refset_env.add obj curr, data, ax2ty)
 
 let traverse current t =
   let () = modcache := MPmap.empty in
-  traverse current [] (Refset.empty, Refmap.empty, Refmap.empty) t
+  traverse current [] (Refset_env.empty, Refmap_env.empty, Refmap_env.empty) t
 
 (** Hopefully bullet-proof function to recover the type of a constant. It just
     ignores all the universe stuff. There are many issues that can arise when
@@ -215,7 +215,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
     let cb = lookup_constant kn in
     if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
-      let l = try Refmap.find obj ax2ty with Not_found -> [] in
+      let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
       ContextObjectMap.add (Axiom (kn,l)) t accu
     else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
       let t = type_of_constant cb in
@@ -227,4 +227,4 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       accu
   | IndRef _ | ConstructRef _ -> accu
   in
-  Refmap.fold fold graph ContextObjectMap.empty
+  Refmap_env.fold fold graph ContextObjectMap.empty
diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli
index a608fe5050..9c9f81bd2f 100644
--- a/toplevel/assumptions.mli
+++ b/toplevel/assumptions.mli
@@ -21,8 +21,8 @@ open Printer
 *)
 val traverse :
   Label.t -> constr ->
-    (Refset.t * Refset.t Refmap.t *
-     (label * Context.rel_context * types) list Refmap.t)
+    (Refset_env.t * Refset_env.t Refmap_env.t *
+     (label * Context.rel_context * types) list Refmap_env.t)
 
 (** Collects all the assumptions (optionally including opaque definitions)
    on which a term relies (together with their type). The above warning of
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 04238da2bd..e2e5d8704e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -77,9 +77,10 @@ let red_constant_entry n ce = function
           (under_binders env
              (fst (reduction_of_red_expr env red)) n body,ctx),eff) }
 
-let interp_definition bl p red_option c ctypopt =
+let interp_definition pl bl p red_option c ctypopt =
   let env = Global.env() in
-  let evdref = ref (Evd.from_env env) in
+  let ctx = Evd.make_evar_universe_context env pl in
+  let evdref = ref (Evd.from_ctx ctx) in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
   let nb_args = List.length ctx in
   let imps,ce =
@@ -92,10 +93,10 @@ let interp_definition bl p red_option c ctypopt =
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
 	let vars = Universes.universes_of_constr body in
-	let ctx = Universes.restrict_universe_context
-	  (Evd.universe_context_set !evdref) vars in
+	let evd = Evd.restrict_universe_context !evdref vars in
+	let uctx = Evd.universe_context ?names:pl evd in
  	imps1@(Impargs.lift_implicits nb_args imps2),
-	  definition_entry ~univs:(Univ.ContextSet.to_context ctx) ~poly:p body
+	  definition_entry ~univs:uctx ~poly:p body
     | Some ctyp ->
 	let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
 	let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -118,11 +119,11 @@ let interp_definition bl p red_option c ctypopt =
 	   strbrk "The term declares more implicits than the type here.");
         let vars = Univ.LSet.union (Universes.universes_of_constr body) 
           (Universes.universes_of_constr typ) in
-        let ctx = Universes.restrict_universe_context
-          (Evd.universe_context_set !evdref) vars in
+        let ctx = Evd.restrict_universe_context !evdref vars in
+	let uctx = Evd.universe_context ?names:pl ctx in
 	imps1@(Impargs.lift_implicits nb_args impsty),
 	  definition_entry ~types:typ ~poly:p 
-	    ~univs:(Univ.ContextSet.to_context ctx) body
+	    ~univs:uctx body
   in
   red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps
 
@@ -172,8 +173,8 @@ let declare_definition ident (local, p, k) ce imps hook =
 
 let _ = Obligations.declare_definition_ref := declare_definition
 
-let do_definition ident k bl red_option c ctypopt hook =
-  let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
+let do_definition ident k pl bl red_option c ctypopt hook =
+  let (ce, evd, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in
     if Flags.is_program_mode () then
       let env = Global.env () in
       let (c,ctx), sideff = Future.force ce.const_entry_body in
@@ -290,6 +291,7 @@ let push_types env idl tl =
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
+  ind_univs : lident list option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -499,7 +501,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     interp_context_evars env0 evdref paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
-
+  let pl = (List.hd indl).ind_univs in
+      
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in
   let params = List.map (fun (na,_,_) -> out_name na) assums in
@@ -541,6 +544,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
   let ctx_params = map_rel_context nf ctx_params in
   let evd = !evdref in
+  let uctx = Evd.universe_context ?names:pl evd in
   List.iter (check_evars env_params Evd.empty evd) arities;
   iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
   List.iter (fun (_,ctyps,_) ->
@@ -568,7 +572,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = Evd.universe_context evd },
+    mind_entry_universes = uctx },
     impls
 
 (* Very syntactical equality *)
@@ -590,8 +594,8 @@ let extract_params indl =
       params
 
 let extract_inductive indl =
-  List.map (fun ((_,indname),_,ar,lc) -> {
-    ind_name = indname;
+  List.map (fun (((_,indname),pl),_,ar,lc) -> {
+    ind_name = indname; ind_univs = pl;
     ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType [])) ar;
     ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
   }) indl
@@ -739,6 +743,7 @@ let check_mutuality env isfix fixl =
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
+  fix_univs : lident list option;
   fix_annot : Id.t Loc.located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
@@ -1066,7 +1071,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
     let init_tac =
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
-    let evd = Evd.from_env ~ctx Environ.empty_env in
+    let evd = Evd.from_ctx ctx in
     Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
       evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
@@ -1102,8 +1107,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
     let init_tac =
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
-    let evd = Evd.from_env ~ctx Environ.empty_env in
-    Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
+    let evd = Evd.from_ctx ctx in
+      Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
       evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
@@ -1130,15 +1135,17 @@ let extract_decreasing_argument limit = function
 
 let extract_fixpoint_components limit l =
   let fixl, ntnl = List.split l in
-  let fixl = List.map (fun ((_,id),ann,bl,typ,def) ->
+  let fixl = List.map (fun (((_,id),pl),ann,bl,typ,def) ->
     let ann = extract_decreasing_argument limit ann in
-      {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
+      {fix_name = id; fix_annot = ann; fix_univs = pl;
+       fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
   fixl, List.flatten ntnl
 
 let extract_cofixpoint_components l =
   let fixl, ntnl = List.split l in
-  List.map (fun ((_,id),bl,typ,def) ->
-    {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
+  List.map (fun (((_,id),pl),bl,typ,def) ->
+	    {fix_name = id; fix_annot = None; fix_univs = pl;
+	     fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
   List.flatten ntnl
 
 let out_def = function
@@ -1191,7 +1198,7 @@ let do_program_recursive local p fixkind fixl ntns =
 let do_program_fixpoint local poly l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
-    | [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
+    | [(n, CWfRec r)], [((((_,id),_),_,bl,typ,def),ntn)] ->
 	let recarg = 
 	  match n with
 	  | Some n -> mkIdentC (snd n)
@@ -1200,7 +1207,7 @@ let do_program_fixpoint local poly l =
 		(str "Recursive argument required for well-founded fixpoints")
 	in build_wellfounded (id, n, bl, typ, out_def def) r recarg ntn
 	     
-    | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
+    | [(n, CMeasureRec (m, r))], [((((_,id),_),_,bl,typ,def),ntn)] ->
 	build_wellfounded (id, n, bl, typ, out_def def)
 	  (Option.default (CRef (lt_ref,None)) r) m ntn
 	  
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 3a38e52cee..f4d43ec533 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -31,14 +31,14 @@ val get_declare_definition_hook : unit -> (definition_entry -> unit)
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  local_binder list -> polymorphic -> red_expr option -> constr_expr ->
+  lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
 val declare_definition : Id.t -> definition_kind ->
   definition_entry -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
-val do_definition : Id.t -> definition_kind ->
+val do_definition : Id.t -> definition_kind -> lident list option ->
   local_binder list -> red_expr option -> constr_expr ->
   constr_expr option -> unit Lemmas.declaration_hook -> unit
 
@@ -70,6 +70,7 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
 
 type structured_one_inductive_expr = {
   ind_name : Id.t;
+  ind_univs : lident list option;
   ind_arity : constr_expr;
   ind_lc : (Id.t * constr_expr) list
 }
@@ -109,6 +110,7 @@ val do_mutual_inductive :
 
 type structured_fixpoint_expr = {
   fix_name : Id.t;
+  fix_univs : lident list option;
   fix_annot : Id.t Loc.located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 738e93e2f9..0b15ecf33e 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -879,7 +879,7 @@ let rec solve_obligation prg num tac =
   in
   let obl = subst_deps_obl obls obl in
   let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
-  let evd = Evd.from_env ~ctx:prg.prg_ctx Environ.empty_env in
+  let evd = Evd.from_ctx prg.prg_ctx in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
   let terminator guard hook = Proof_global.make_terminator (obligation_terminator prg.prg_name num guard hook) in
   let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 15ad18d9cc..484fd081df 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -90,9 +90,10 @@ let binder_of_decl = function
 
 let binders_of_decls = List.map binder_of_decl
 
-let typecheck_params_and_fields def id t ps nots fs =
+let typecheck_params_and_fields def id pl t ps nots fs =
   let env0 = Global.env () in
-  let evars = ref (Evd.from_env env0) in
+  let ctx = Evd.make_evar_universe_context env0 pl in
+  let evars = ref (Evd.from_ctx ctx) in
   let _ = 
     let error bk (loc, name) = 
       match bk, name with
@@ -502,7 +503,7 @@ open Vernacexpr
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions 
    or subinstances *)
-let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let cfs,priorities = List.split cfs in
   let coers,fs = List.split cfs in
@@ -519,7 +520,7 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild
   (* Now, younger decl in params and fields is on top *)
   let ctx, arity, template, implpars, params, implfs, fields =
     States.with_state_protection (fun () ->
-      typecheck_params_and_fields (kind = Class true) idstruc s ps notations fs) () in
+      typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
     match kind with
     | Class def ->
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 91dccb96e1..eccb5d29d6 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -38,7 +38,7 @@ val declare_structure : Decl_kinds.recursivity_kind ->
   inductive
 
 val definition_structure :
-  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * lident with_coercion * local_binder list *
+  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cfbdaccec4..8efcccaaae 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -461,7 +461,7 @@ let vernac_definition_hook p = function
 | SubClass -> Class.add_subclass_hook p
 | _ -> no_hook
 
-let vernac_definition locality p (local,k) (loc,id as lid) def =
+let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   let local = enforce_locality_exp locality local in
   let hook = vernac_definition_hook p k in
   let () = match local with
@@ -471,20 +471,20 @@ let vernac_definition locality p (local,k) (loc,id as lid) def =
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
  	  start_proof_and_print (local,p,DefinitionBody Definition)
-	    [Some lid, (bl,t,None)] no_hook
+	    [Some (lid,pl), (bl,t,None)] no_hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
           | Some r ->
 	      let (evc,env)= get_current_context () in
  		Some (snd (interp_redexp env evc r)) in
-	do_definition id (local,p,k) bl red_option c typ_opt hook)
+	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof p kind l lettop =
   if Dumpglob.dump () then
     List.iter (fun (id, _) ->
       match id with
-	| Some lid -> Dumpglob.dump_definition lid false "prf"
+	| Some (lid,_) -> Dumpglob.dump_definition lid false "prf"
 	| None -> ()) l;
   if not(refining ()) then
     if lettop then
@@ -525,11 +525,11 @@ let vernac_assumption locality poly (local, kind) l nl =
 
 let vernac_record k poly finite struc binders sort nameopt cfs =
   let const = match nameopt with
-    | None -> add_prefix "Build_" (snd (snd struc))
+    | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
 	Dumpglob.dump_definition lid false "constr"; id in
     if Dumpglob.dump () then (
-      Dumpglob.dump_definition (snd struc) false "rec";
+      Dumpglob.dump_definition (fst (snd struc)) false "rec";
       List.iter (fun (((_, x), _), _) ->
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
@@ -538,7 +538,7 @@ let vernac_record k poly finite struc binders sort nameopt cfs =
 
 let vernac_inductive poly lo finite indl =
   if Dumpglob.dump () then
-    List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
+    List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
 	| Constructors cstrs ->
 	    Dumpglob.dump_definition lid false "ind";
@@ -578,13 +578,13 @@ let vernac_inductive poly lo finite indl =
 let vernac_fixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
-    List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+    List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_fixpoint local poly l
 
 let vernac_cofixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
-    List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+    List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_cofixpoint local poly l
 
 let vernac_scheme l =