Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

25 files changed, 218 insertions, 406 deletions

diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 5dbd5379..80787298 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Names
 open Ind_tables
 
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 22ea09c5..b29ba1ef 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Pp
 open Errors
 open Indtypes
@@ -53,12 +52,15 @@ let _ = Errors.register_handler explain_exn_default
 
 (** Pre-explain a vernac interpretation error *)
 
-let wrap_vernac_error (exn, info) strm =
-  let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
-  let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
-  (e, info)
+let wrap_vernac_error with_header (exn, info) strm =
+  if with_header then
+    let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
+    let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
+    (e, info)
+  else
+    (EvaluatedError (strm, None), info)
 
-let process_vernac_interp_error exn = match fst exn with
+let process_vernac_interp_error with_header exn = match fst exn with
   | Univ.UniverseInconsistency i ->
     let msg =
       if !Constrextern.print_universes then
@@ -66,40 +68,40 @@ let process_vernac_interp_error exn = match fst exn with
 	  Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
       else
 	mt() in
-    wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
+    wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".")
   | TypeError(ctx,te) ->
-      wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
+      wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te)
   | PretypeError(ctx,sigma,te) ->
-      wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
+      wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
-      wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+      wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te)
   | InductiveError e ->
-      wrap_vernac_error exn (Himsg.explain_inductive_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_inductive_error e)
   | Modops.ModuleTypingError e ->
-      wrap_vernac_error exn (Himsg.explain_module_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_module_error e)
   | Modintern.ModuleInternalizationError e ->
-      wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e)
   | RecursionSchemeError e ->
-      wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e)
   | Cases.PatternMatchingError (env,sigma,e) ->
-      wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e)
+      wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e)
   | Tacred.ReductionTacticError e ->
-      wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e ->
-      wrap_vernac_error exn (Himsg.explain_refiner_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_refiner_error e)
   | Nametab.GlobalizationError q ->
-      wrap_vernac_error exn
+      wrap_vernac_error with_header exn
         (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
 	 spc () ++ str "was not found" ++
 	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
   | Refiner.FailError (i,s) ->
       let s = Lazy.force s in
-      wrap_vernac_error exn
+      wrap_vernac_error with_header exn
 	(str "Tactic failure" ++
          (if Pp.is_empty s then s else str ": " ++ s) ++
          if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
-      wrap_vernac_error exn (msg ++ str ".")
+      wrap_vernac_error with_header exn (msg ++ str ".")
   | _ ->
       exn
 
@@ -108,9 +110,9 @@ let rec strip_wrapping_exceptions = function
     strip_wrapping_exceptions e
   | exc -> exc
 
-let process_vernac_interp_error (exc, info) =
+let process_vernac_interp_error ?(with_header=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
-  let e = process_vernac_interp_error (exc, info) in
+  let e = process_vernac_interp_error with_header (exc, info) in
   let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   match ltac_trace with
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 1768af11..100b3772 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : Util.iexn -> Util.iexn
+val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index f44ac367..33891ad9 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -103,8 +103,13 @@ let instance_hook k pri global imps ?hook cst =
 
 let declare_instance_constant k pri global imps ?hook id poly uctx term termtype =
   let kind = IsDefinition Instance in
+  let uctx = 
+    let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
+				 (Universes.universes_of_constr term) in
+      Universes.restrict_universe_context uctx levels 
+  in
   let entry = 
-    Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
+    Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term
   in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
@@ -165,7 +170,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
   in
   let env' = push_rel_context ctx env in
   evars := Evarutil.nf_evar_map !evars;
-  evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars;
+  evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars;
   let subst = List.map (Evarutil.nf_evar !evars) subst in
     if abstract then
       begin
@@ -208,7 +213,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    let get_id =
 	      function
 		| Ident id' -> id'
-		| _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled")
+		| Qualid (loc,id') -> (loc, snd (repr_qualid id'))
 	    in
 	    let props, rest =
 	      List.fold_left
@@ -232,7 +237,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, Misctypes.IntroAnonymous, None) :: props), rest
+		       (CHole (Loc.ghost, None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
@@ -277,7 +282,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
       in
       let term = Option.map nf term in
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
-          let ctx = Evd.universe_context evm in
+          let ctx = Evd.universe_context_set evm in
 	  declare_instance_constant k pri global imps ?hook id 
             poly ctx (Option.get term) termtype
 	else if !refine_instance || Option.is_empty term then begin
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 0a351d3c..2b7e9e4f 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Context
-open Evd
 open Environ
 open Constrexpr
 open Typeclasses
@@ -33,7 +32,7 @@ val declare_instance_constant :
   ?hook:(Globnames.global_reference -> unit) ->
   Id.t -> (** name *)
   bool -> (* polymorphic *)
-  Univ.universe_context -> (* Universes *)
+  Univ.universe_context_set -> (* Universes *)
   Constr.t -> (** body *)
   Term.types -> (** type *)
   Names.Id.t
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9cb3bb86..754ad852 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -233,9 +233,9 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma
   in
     (gr,inst,Lib.is_modtype_strict ())
 
-let interp_assumption evdref env bl c =
+let interp_assumption evdref env impls bl c =
   let c = prod_constr_expr c bl in
-  let ty, impls = interp_type_evars_impls env evdref c in
+  let ty, impls = interp_type_evars_impls env evdref ~impls c in
   let evd, nf = nf_evars_and_universes !evdref in
   let ctx = Evd.universe_context_set evd in
     ((nf ty, ctx), impls)
@@ -259,12 +259,15 @@ let do_assumptions (_, poly, _ as kind) nl l =
         l []
     else l
   in
-  let _,l = List.fold_map (fun env (is_coe,(idl,c)) ->
-    let (t,ctx),imps = interp_assumption evdref env [] c in
+  let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) ->
+    let (t,ctx),imps = interp_assumption evdref env ienv [] c in
     let env =
       push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in
-      (env,((is_coe,idl),t,(ctx,imps)))) 
-    env l 
+    let ienv = List.fold_right (fun (_,id) ienv ->
+      let impls = compute_internalization_data env Variable t imps in
+      Id.Map.add id impls ienv) idl ienv in
+      ((env,ienv),((is_coe,idl),t,(ctx,imps)))) 
+    (env,empty_internalization_env) l
   in
   let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in
   let l = List.map (on_pi2 (nf_evar evd)) l in
@@ -746,8 +749,8 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
-  let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
+let declare_fix ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
+  let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
   declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref := declare_fix
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 894333ad..3a38e52c 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -11,7 +11,6 @@ open Term
 open Entries
 open Libnames
 open Globnames
-open Tacexpr
 open Vernacexpr
 open Constrexpr
 open Decl_kinds
@@ -167,5 +166,5 @@ val do_cofixpoint :
 
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
-val declare_fix : definition_kind -> Univ.universe_context -> Id.t ->
+val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
   Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 03074ced..f1d8a492 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -57,28 +57,20 @@ let load_rcfile() =
   else
     Flags.if_verbose msg_info (str"Skipping rcfile loading.")
 
-(* Puts dir in the path of ML and in the LoadPath *)
-let coq_add_path unix_path s =
-  Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true;
-  Mltop.add_ml_dir unix_path
-
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let add_stdlib_path ~unix_path ~coq_root ~with_ml =
-  if !Flags.load_init then
-    Mltop.add_rec_path ~unix_path ~coq_root ~implicit:true
-  else
-    Mltop.add_path ~unix_path ~coq_root ~implicit:false;
+  Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init);
   if with_ml then
     Mltop.add_rec_ml_dir unix_path
 
 let add_userlib_path ~unix_path =
-  Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false;
+  Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false;
   Mltop.add_rec_ml_dir unix_path
 
 (* Options -I, -I-as, and -R of the command line *)
 let includes = ref []
-let push_include s alias recursive implicit =
-  includes := (s,alias,recursive,implicit) :: !includes
+let push_include s alias implicit =
+  includes := (s, alias, implicit) :: !includes
 let ml_includes = ref []
 let push_ml_include s = ml_includes := s :: !ml_includes
 
@@ -91,10 +83,11 @@ let init_load_path () =
   let coq_root = Names.DirPath.make [Nameops.coq_root] in
     (* NOTE: These directories are searched from last to first *)
     (* first, developer specific directory to open *)
-    if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
+    if Coq_config.local then
+      Mltop.add_ml_dir (coqlib/"dev");
     (* main loops *)
     if Coq_config.local || !Flags.boot then begin
-      let () = Mltop.add_ml_dir (coqlib/"stm") in
+      Mltop.add_ml_dir (coqlib/"stm");
       Mltop.add_ml_dir (coqlib/"ide")
     end;
     Mltop.add_ml_dir (coqlib/"toploop");
@@ -109,13 +102,13 @@ let init_load_path () =
     List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs;
     (* then directories in COQPATH *)
     List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath;
-    (* then current directory *)
-    Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix ~implicit:false;
-    (* additional loadpath, given with options -I-as, -Q, and -R *)
+    (* then current directory (not recursively!) *)
+    Mltop.add_ml_dir ".";
+    Loadpath.add_load_path "." Nameops.default_root_prefix ~implicit:false;
+    (* additional loadpath, given with options -Q and -R *)
     List.iter
-      (fun (unix_path, coq_root, reci, implicit) ->
-        (if reci then Mltop.add_rec_path else Mltop.add_path)
-          ~unix_path ~coq_root ~implicit)
+      (fun (unix_path, coq_root, implicit) ->
+        Mltop.add_rec_path ~unix_path ~coq_root ~implicit)
       (List.rev !includes);
     (* additional ml directories, given with option -I *)
     List.iter Mltop.add_ml_dir (List.rev !ml_includes)
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 5f7133c3..c019cc1c 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -15,8 +15,8 @@ val set_rcfile : string -> unit
 val no_load_rc : unit -> unit
 val load_rcfile : unit -> unit
 
-val push_include : string -> Names.DirPath.t -> bool -> bool -> unit
-(** [push_include phys_path log_path recursive implicit] *)
+val push_include : string -> Names.DirPath.t -> bool -> unit
+(** [push_include phys_path log_path implicit] *)
 
 val push_ml_include : string -> unit
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 142f3386..e9e86953 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -135,9 +135,9 @@ let set_outputstate s =
   outputstate:=s
 let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
 
-let set_include d p recursive implicit =
+let set_include d p implicit =
   let p = dirpath_of_string p in
-  push_include d p recursive implicit
+  push_include d p implicit
 
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
@@ -378,7 +378,7 @@ let schedule_vio_compilation () =
 let get_native_name s =
   (* We ignore even critical errors because this mode has to be super silent *)
   try
-    String.concat Filename.dir_sep [Filename.dirname s;
+    String.concat "/" [Filename.dirname s;
       Nativelib.output_dir; Library.native_name_from_filename s]
   with _ -> ""
 
@@ -402,21 +402,21 @@ let parse_args arglist =
     (* Complex options with many args *)
     |"-I"|"-include" ->
       begin match rem with
-      | d :: "-as" :: p :: rem -> set_include d p false true; args := rem
-      | d :: "-as" :: [] -> error_missing_arg "-as"
       | d :: rem -> push_ml_include d; args := rem
       | [] -> error_missing_arg opt
       end
     |"-Q" ->
       begin match rem with
-      | d :: p :: rem -> set_include d p true false; args := rem
+      | d :: p :: rem -> set_include d p false; args := rem
       | _ -> error_missing_arg opt
       end
     |"-R" ->
       begin match rem with
-      | d :: "-as" :: [] -> error_missing_arg "-as"
-      | d :: "-as" :: p :: rem
-      | d :: p :: rem -> set_include d p true true; args := rem
+      | d :: "-as" :: [] -> error_missing_arg opt
+      | d :: "-as" :: p :: rem ->
+        warning "option -R * -as * deprecated, remove the -as";
+        set_include d p true; args := rem
+      | d :: p :: rem -> set_include d p true; args := rem
       | _ -> error_missing_arg opt
       end
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 9341f2f7..5429e660 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -879,7 +879,9 @@ let explain_label_already_declared l =
   str ("The label "^Label.to_string l^" is already declared.")
 
 let explain_application_to_not_path _ =
-  str "Application of modules is restricted to paths."
+  strbrk "A module cannot be applied to another module application or " ++
+  strbrk "with-expression; you must give a name to the intermediate result " ++
+  strbrk "module first."
 
 let explain_not_a_functor () =
   str "Application of a non-functor."
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index e6b23828..fbc45b4a 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -85,7 +85,7 @@ let _ =
     { optsync  = true;
       optdepr  = false;
       optname  = "automatic declaration of boolean equality";
-      optkey   = ["Equality";"Schemes"];
+      optkey   = ["Boolean";"Equality";"Schemes"];
       optread  = (fun () -> !eq_flag) ;
       optwrite = (fun b -> eq_flag := b) }
 let _ = (* compatibility *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 161cf824..639ec1e6 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -61,23 +61,42 @@ let rec make_tags = function
   | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l
   | [] -> []
 
+let make_fresh_key =
+  let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
+  fun () ->
+    let cur = incr id; !id in
+    let lbl = Id.of_string ("_" ^ string_of_int cur) in
+    let kn = Lib.make_kn lbl in
+    let (mp, dir, _) = KerName.repr kn in
+    (** We embed the full path of the kernel name in the label so that the
+        identifier should be unique. This ensures that including two modules
+        together won't confuse the corresponding labels. *)
+    let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
+      (ModPath.to_string mp) (DirPath.to_string dir) cur)
+    in
+    KerName.make mp dir (Label.of_id lbl)
+
 type tactic_grammar_obj = {
+  tacobj_key : KerName.t;
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
   tacobj_tacpp : Pptactic.pp_tactic;
   tacobj_body : Tacexpr.glob_tactic_expr
 }
 
-let cache_tactic_notation ((_, key), tobj) =
+let cache_tactic_notation (_, tobj) =
+  let key = tobj.tacobj_key in
   Tacenv.register_alias key tobj.tacobj_body;
   Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
 
-let open_tactic_notation i ((_, key), tobj) =
+let open_tactic_notation i (_, tobj) =
+  let key = tobj.tacobj_key in
   if Int.equal i 1 && not tobj.tacobj_local then
     Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
 
-let load_tactic_notation i ((_, key), tobj) =
+let load_tactic_notation i (_, tobj) =
+  let key = tobj.tacobj_key in
   (** Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
@@ -85,7 +104,10 @@ let load_tactic_notation i ((_, key), tobj) =
     Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
 
 let subst_tactic_notation (subst, tobj) =
-  { tobj with tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; }
+  { tobj with
+    tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
+    tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body;
+  }
 
 let classify_tactic_notation tacobj = Substitute tacobj
 
@@ -115,6 +137,7 @@ let add_tactic_notation (local,n,prods,e) =
     tacgram_prods = prods;
   } in
   let tacobj = {
+    tacobj_key = make_fresh_key ();
     tacobj_local = local;
     tacobj_tacgram = parule;
     tacobj_tacpp = pprule;
@@ -1103,7 +1126,7 @@ let open_notation i (_, nobj) =
   let scope = nobj.notobj_scope in
   let (ntn, df) = nobj.notobj_notation in
   let pat = nobj.notobj_interp in
-  if Int.equal i 1 then begin
+  if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin
     (* Declare the interpretation *)
     Notation.declare_notation_interpretation ntn scope pat df;
     (* Declare the uninterpretation *)
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 9dc1dd5b..0b6fc48c 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -161,17 +161,6 @@ let add_rec_ml_dir unix_path =
 
 (* Adding files to Coq and ML loadpath *)
 
-let add_path ~unix_path:dir ~coq_root:coq_dirpath ~implicit =
-  if exists_dir dir then
-    begin
-      add_ml_dir dir;
-      Loadpath.add_load_path dir
-        (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath)
-        coq_dirpath
-    end
-  else
-    msg_warning (str ("Cannot open " ^ dir))
-
 let convert_string d =
   try Names.Id.of_string d
   with UserError _ ->
@@ -191,11 +180,9 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
     let dirs = List.map_filter convert_dirs dirs in
     let () = add_ml_dir unix_path in
     let add (path, dir) =
-      Loadpath.add_load_path path Loadpath.ImplicitPath dir in
-    let () = if implicit then List.iter add dirs in
-    Loadpath.add_load_path unix_path
-      (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath)
-      coq_root
+      Loadpath.add_load_path path ~implicit dir in
+    let () = List.iter add dirs in
+    Loadpath.add_load_path unix_path ~implicit coq_root
   else
     msg_warning (str ("Cannot open " ^ unix_path))
 
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 2a91afd8..4f3f4ddd 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -47,7 +47,6 @@ val add_ml_dir : string -> unit
 val add_rec_ml_dir : string -> unit
 
 (** Adds a path to the Coq and ML paths *)
-val add_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
 val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
 
 (** List of modules linked to the toplevel *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index aa068586..523134b5 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -21,7 +21,7 @@ open Pp
 open Errors
 open Util
 
-let declare_fix_ref = ref (fun _ _ _ _ _ _ -> assert false)
+let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
 let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
 
 let trace s =
@@ -319,6 +319,7 @@ type program_info = {
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
   prg_hook : unit Lemmas.declaration_hook;
+  prg_opaque : bool;
 }
 
 let assumption_message = Declare.assumption_message
@@ -512,8 +513,9 @@ let declare_definition prg =
   let body, typ = subst_body true prg in
   let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
     (Evd.evar_universe_context_subst prg.prg_ctx) in
+  let opaque = prg.prg_opaque in
   let ce =
-    definition_entry ~types:(nf typ) ~poly:(pi2 prg.prg_kind) 
+    definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
       ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
     progmap_remove prg;
@@ -564,6 +566,7 @@ let declare_mutual_definition l =
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
   let (local,poly,kind) = first.prg_kind in
   let fixnames = first.prg_deps in
+  let opaque = first.prg_opaque in
   let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
   let indexes, fixdecls =
     match fixkind with
@@ -584,7 +587,7 @@ let declare_mutual_definition l =
   in
   (* Declare the recursive definitions *)
   let ctx = Evd.evar_context_universe_context first.prg_ctx in
-  let kns = List.map4 (!declare_fix_ref (local, poly, kind) ctx) 
+  let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter Metasyntax.add_notation_interpretation first.prg_notations;
@@ -640,7 +643,7 @@ let declare_obligation prg obl body ty uctx =
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
 
-let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook =
+let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls kind reduce hook =
   let obls', b = 
     match b with
     | None ->
@@ -655,7 +658,7 @@ let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook
 	Array.mapi
 	  (fun i (n, t, l, o, d, tac) ->
             { obl_name = n ; obl_body = None; 
-	      obl_location = l; obl_type = reduce t; obl_status = o;
+	      obl_location = l; obl_type = t; obl_status = o;
 	      obl_deps = d; obl_tac = tac })
 	  obls, b
   in
@@ -664,7 +667,8 @@ let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
-      prg_hook = hook; }
+      prg_hook = hook;
+      prg_opaque = opaque; }
 
 let get_prog name =
   let prg_infos = !from_prg in
@@ -976,9 +980,9 @@ let show_term n =
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
 let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) obls =
+    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls =
   let info = str (Id.to_string n) ++ str " has type-checked" in
-  let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
+  let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose msg_info (info ++ str ".");
@@ -994,11 +998,11 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=Lemmas.mk_hook (fun _ _ -> ())) notations fixkind =
+    ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info n (Some b) t ctx deps (Some fixkind) 
+     let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
      in progmap_add n prg) l;
     let _defined =
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 582b4935..40f124ca 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -14,10 +14,9 @@ open Pp
 open Globnames
 open Vernacexpr
 open Decl_kinds
-open Tacexpr
 
 (** Forward declaration. *)
-val declare_fix_ref : (definition_kind -> Univ.universe_context -> Id.t ->
+val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
   Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
 
 val declare_definition_ref :
@@ -69,7 +68,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook -> obligation_info -> progress
+  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -85,7 +84,7 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook ->
+  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 55f53351..737b7fb5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -472,10 +472,15 @@ let add_inductive_class ind =
   let k =
     let ctx = oneind.mind_arity_ctxt in
     let inst = Univ.UContext.instance mind.mind_universes in
+    let map = function
+    | (_, Some _, _) -> None
+    | (_, None, t) -> Some (lazy t)
+    in
+    let args = List.map_filter map ctx in
     let ty = Inductive.type_of_inductive_knowing_parameters
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
-      (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx))
+      (Array.of_list args)
     in
       { cl_impl = IndRef ind;
 	cl_context = List.map (const None) ctx, ctx;
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index d22524e5..bf0f305a 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -13,7 +13,6 @@ Record
 Vernacinterp
 Mltop
 Vernacentries
-Whelp
 Vernac
 Usage
 Coqloop
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index d4d44569..f053839c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -23,9 +23,7 @@ let print_usage_channel co command =
   output_string co
 "  -I dir                 look for ML files in dir\
 \n  -include dir           (idem)\
-\n  -I dir -as coqdir      implicitly map physical dir to logical coqdir\
-\n  -R dir -as coqdir      recursively map physical dir to logical coqdir\
-\n  -R dir coqdir          (idem)\
+\n  -R dir coqdir          recursively map physical dir to logical coqdir\
 \n  -Q dir coqdir          map physical dir to logical coqdir\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\
 \n  -notop                 set the toplevel name to be the empty logical path\
@@ -47,6 +45,11 @@ let print_usage_channel co command =
 \n  -require f             load Coq object file f.vo and import it (Require f.)\
 \n  -compile f             compile Coq file f.v (implies -batch)\
 \n  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)\
+\n  -quick                 quickly compile .v files to .vio files (skip proofs)\
+\n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
+\n                         into fi.vo\
+\n  -schedule-vio-checking j f1..fn   run up to j instances of Coq to check all\
+\n                         proofs in each fi.vio\
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config                print Coq's configuration information and exit\
@@ -66,6 +69,7 @@ let print_usage_channel co command =
 \n  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
 \n  -impredicative-set     set sort Set impredicative\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
+\n  -type-in-type          disable universe consistency checking\
 \n  -time                  display the time taken by each command\
 \n  -no-native-compiler    disable the native_compute reduction machinery\
 \n  -h, -help              print this list of options\
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fb12edfb..cfa9bddc 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -387,12 +387,13 @@ let err_unmapped_library loc qid =
        pr_dirpath dir ++ str".")
 
 let err_notfound_library loc qid =
-  msg_error
-    (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid ++ str"."))
+  user_err_loc
+    (loc,"locate_library",
+     strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")
 
 let print_located_library r =
   let (loc,qid) = qualid_of_reference r in
-  try msg_found_library (Library.locate_qualified_library false qid)
+  try msg_found_library (Library.locate_qualified_library ~warn:false qid)
   with
     | Library.LibUnmappedDir -> err_unmapped_library loc qid
     | Library.LibNotFound -> err_notfound_library loc qid
@@ -496,7 +497,7 @@ let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
   let status = by (Tactics.New.exact_proof c) in
-  save_proof (Vernacexpr.Proved(true,None));
+  save_proof (Vernacexpr.(Proved(Opaque None,None)));
   if not status then Pp.feedback Feedback.AddedAxiom
 
 let vernac_assumption locality poly (local, kind) l nl =
@@ -598,11 +599,8 @@ let vernac_constraint l = do_constraint l
 (* Modules            *)
 
 let vernac_import export refl =
-  let import ref =
-    Library.import_module export (qualid_of_reference ref)
-  in
-    List.iter import refl;
-    Lib.add_frozen_state ()
+  Library.import_module export (List.map qualid_of_reference refl);
+  Lib.add_frozen_state ()
 
 let vernac_declare_module export (loc, id) binders_ast mty_ast =
   (* We check the state of the system (in section, in module type)
@@ -752,9 +750,25 @@ let vernac_end_segment (_,id as lid) =
 
 (* Libraries *)
 
-let vernac_require import qidl =
+let vernac_require from import qidl =
   let qidl = List.map qualid_of_reference qidl in
-  let modrefl = List.map Library.try_locate_qualified_library qidl in
+  let root = match from with
+  | None -> None
+  | Some from ->
+    let (_, qid) = Libnames.qualid_of_reference from in
+    let (hd, tl) = Libnames.repr_qualid qid in
+    Some (Libnames.add_dirpath_suffix hd tl)
+  in
+  let locate (loc, qid) =
+    try
+      let warn = Flags.is_verbose () in
+      let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
+      (dir, f)
+    with
+      | Library.LibUnmappedDir -> err_unmapped_library loc qid
+      | Library.LibNotFound -> err_notfound_library loc qid
+  in
+  let modrefl = List.map locate qidl in
   if Dumpglob.dump () then
     List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl);
   Library.require_library_from_dirpath modrefl import
@@ -878,11 +892,10 @@ let vernac_set_used_variables e =
 let expand filename =
   Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename
 
-let vernac_add_loadpath isrec pdir ldiropt =
+let vernac_add_loadpath implicit pdir ldiropt =
   let pdir = expand pdir in
   let alias = Option.default Nameops.default_root_prefix ldiropt in
-  (if isrec then Mltop.add_rec_path else Mltop.add_path)
-    ~unix_path:pdir ~coq_root:alias ~implicit:true
+  Mltop.add_rec_path ~unix_path:pdir ~coq_root:alias ~implicit
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)
@@ -963,20 +976,27 @@ let register_ltac local isrec tacl =
     (name, body)
   in
   let rfun = List.map map tacl in
-  let ltacrecvars =
+  let recvars =
     let fold accu (op, _) = match op with
     | UpdateTac _ -> accu
-    | NewTac id -> Id.Map.add id (Lib.make_kn id) accu
+    | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
     in
-    if isrec then List.fold_left fold Id.Map.empty rfun
-    else Id.Map.empty
+    if isrec then List.fold_left fold [] rfun
+    else []
   in
-  let ist = { (Tacintern.make_empty_glob_sign ()) with Genintern.ltacrecvars; } in
+  let ist = Tacintern.make_empty_glob_sign () in
   let map (name, body) =
     let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
     (name, body)
   in
-  let defs = List.map map rfun in
+  let defs () =
+    (** Register locally the tactic to handle recursivity. This function affects
+        the whole environment, so that we transactify it afterwards. *)
+    let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
+    let () = List.iter iter_rec recvars in
+    List.map map rfun
+  in
+  let defs = Future.transactify defs () in
   let iter (def, tac) = match def with
   | NewTac id ->
     Tacenv.register_ltac false local id tac;
@@ -1124,6 +1144,7 @@ let vernac_declare_arguments locality r l nargs flags =
     vernac_declare_implicits locality r implicits;
   if nargs >= 0 && nargs < List.fold_left max 0 rargs then
     error "The \"/\" option must be placed after the last \"!\".";
+  let no_flags = List.is_empty flags in
   let rec narrow = function
     | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl
     | [] -> [] | _ :: tl -> narrow tl in
@@ -1141,7 +1162,7 @@ let vernac_declare_arguments locality r l nargs flags =
           some_implicits_specified ||
           some_scopes_specified ||
           some_simpl_flags_specified) &&
-     List.length flags = 0 then
+     no_flags then
     msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'")
 
 
@@ -1503,7 +1524,7 @@ let vernac_check_may_eval redexp glopt rc =
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
   let uctx = Evd.universe_context sigma' in
-  let env = Environ.push_context uctx env in
+  let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
   let c = nf c in
   let j =
     if Evarutil.has_undefined_evars sigma' c then
@@ -1516,12 +1537,8 @@ let vernac_check_may_eval redexp glopt rc =
         let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
         let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
 	msg_notice (print_judgment env sigma' j ++
-                    (if l != Evar.Set.empty then
-                        let l = Evar.Set.fold (fun ev -> Evar.Map.add ev (Evarutil.nf_evar_info sigma' (Evd.find sigma' ev))) l Evar.Map.empty in
-                        (fnl () ++ str "where" ++ fnl () ++ pr_evars sigma' l)
-                     else
-                        mt ()) ++
-                     Printer.pr_universe_ctx uctx)
+                    pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
+                    Printer.pr_universe_ctx uctx)
     | Some r ->
         Tacintern.dump_glob_red_expr r;
         let (sigma',r_interp) = interp_redexp env sigma' r in
@@ -1883,7 +1900,7 @@ let interp ?proof locality poly c =
 
   | VernacNameSectionHypSet (lid, set) -> vernac_name_sec_hyp lid set
 
-  | VernacRequire (export, qidl) -> vernac_require export qidl
+  | VernacRequire (from, export, qidl) -> vernac_require from export qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
   | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t
@@ -1951,14 +1968,16 @@ let interp ?proof locality poly c =
   | VernacComments l -> if_verbose msg_info (str "Comments ok\n")
   | VernacNop -> ()
 
+  (* The STM should handle that, but LOAD bypasses the STM... *)
+  | VernacAbort id -> msg_warning (str "VernacAbort not handled by Stm")
+  | VernacAbortAll -> msg_warning (str "VernacAbortAll not handled by Stm")
+  | VernacRestart -> msg_warning (str "VernacRestart not handled by Stm")
+  | VernacUndo _ -> msg_warning (str "VernacUndo not handled by Stm")
+  | VernacUndoTo _ -> msg_warning (str "VernacUndoTo not handled by Stm")
+  | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm")
+  
   (* Proof management *)
   | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false
-  | VernacAbort id -> anomaly (str "VernacAbort not handled by Stm")
-  | VernacAbortAll -> anomaly (str "VernacAbortAll not handled by Stm")
-  | VernacRestart -> anomaly (str "VernacRestart not handled by Stm")
-  | VernacUndo _ -> anomaly (str "VernacUndo not handled by Stm")
-  | VernacUndoTo _ -> anomaly (str "VernacUndoTo not handled by Stm")
-  | VernacBacktrack _ -> anomaly (str "VernacBacktrack not handled by Stm")
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()
@@ -2061,7 +2080,7 @@ let locate_if_not_already loc (e, info) =
   | Some l -> if Loc.is_ghost l then (e, Loc.add_loc info loc) else (e, info)
 
 exception HasNotFailed
-exception HasFailed of string
+exception HasFailed of std_ppcmds
 
 let with_fail b f =
   if not b then f ()
@@ -2076,8 +2095,8 @@ let with_fail b f =
            | HasNotFailed as e -> raise e
            | e ->
               let e = Errors.push e in
-              raise (HasFailed (Pp.string_of_ppcmds
-              (Errors.iprint (Cerrors.process_vernac_interp_error e)))))
+              raise (HasFailed (Errors.iprint
+                (Cerrors.process_vernac_interp_error ~with_header:false e))))
         ()
     with e when Errors.noncritical e -> 
       let (e, _) = Errors.push e in
@@ -2086,8 +2105,7 @@ let with_fail b f =
           errorlabstrm "Fail" (str "The command has not failed!")
       | HasFailed msg ->
           if is_verbose () || !Flags.ide_slave then msg_info
-    	(str "The command has indeed failed with message:" ++
-    	 fnl () ++ str "=> " ++ hov 0 (str msg))
+            (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end
 
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 17f971fd..d3e48f75 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -10,14 +10,17 @@ open Util
 open Pp
 open Errors
 
+type deprecation = bool
+type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
+
 (* Table of vernac entries *)
 let vernac_tab =
   (Hashtbl.create 51 :
-    (Vernacexpr.extend_name, (Genarg.raw_generic_argument list -> unit -> unit)) Hashtbl.t)
+    (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t)
 
-let vinterp_add s f =
+let vinterp_add depr s f =
   try
-    Hashtbl.add vernac_tab s f
+    Hashtbl.add vernac_tab s (depr, f)
   with Failure _ ->
     errorlabstrm "vinterp_add"
       (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
@@ -28,7 +31,7 @@ let overwriting_vinterp_add s f =
       let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s
     with Not_found -> ()
   end;
-  Hashtbl.add vernac_tab s f
+  Hashtbl.add vernac_tab s (false, f)
 
 let vinterp_map s =
   try
@@ -44,7 +47,16 @@ let vinterp_init () = Hashtbl.clear vernac_tab
 let call ?locality (opn,converted_args) =
   let loc = ref "Looking up command" in
   try
-    let callback = vinterp_map opn in
+    let depr, callback = vinterp_map opn in
+    let () = if depr then
+      let rules = Egramml.get_extend_vernac_rule opn in
+      let pr_gram = function
+      | Egramml.GramTerminal s -> str s
+      | Egramml.GramNonTerminal _ -> str "_"
+      in
+      let pr = pr_sequence pr_gram rules in
+      msg_warning (str "Deprecated vernacular command: " ++ pr)
+    in
     loc:= "Checking arguments";
     let hunk = callback converted_args in
     loc:= "Executing command";
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 38fce5d1..02820654 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -8,9 +8,13 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-val vinterp_add : Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
+type deprecation = bool
+type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
+
+val vinterp_add : deprecation -> Vernacexpr.extend_name ->
+  vernac_command -> unit
 val overwriting_vinterp_add :
-  Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
+  Vernacexpr.extend_name -> vernac_command -> unit
 
 val vinterp_init : unit -> unit
 val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
deleted file mode 100644
index daedc30f..00000000
--- a/toplevel/whelp.ml4
+++ /dev/null
@@ -1,224 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open Flags
-open Pp
-open Errors
-open Names
-open Term
-open Glob_term
-open Libnames
-open Globnames
-open Nametab
-open Detyping
-open Constrintern
-open Dischargedhypsmap
-open Pfedit
-open Tacmach
-open Misctypes
-
-(* Coq interface to the Whelp query engine developed at
-   the University of Bologna *)
-
-let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080"
-let getter_server_name = ref "http://mowgli.cs.unibo.it:58081"
-
-open Goptions
-
-let _ =
-  declare_string_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "Whelp server";
-      optkey   = ["Whelp";"Server"];
-      optread  = (fun () -> !whelp_server_name);
-      optwrite = (fun s -> whelp_server_name := s) }
-
-let _ =
-  declare_string_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "Whelp getter";
-      optkey   = ["Whelp";"Getter"];
-      optread  = (fun () -> !getter_server_name);
-      optwrite = (fun s -> getter_server_name := s) }
-
-
-let make_whelp_request req c =
-  !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
-
-let b = Buffer.create 16
-
-let url_char c =
-  if 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' ||
-     '0' <= c && c <= '9' || c ='.'
-  then Buffer.add_char b c
-  else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c))
-
-let url_string s = String.iter url_char s
-
-let rec url_list_with_sep sep f = function
-  | [] -> ()
-  | [a] -> f a
-  | a::l -> f a; url_string sep; url_list_with_sep sep f l
-
-let url_id id = url_string (Id.to_string id)
-
-let uri_of_dirpath dir =
-  url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir)
-
-let error_whelp_unknown_reference ref =
-  let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
-  errorlabstrm ""
-    (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++
-     strbrk ", are not supported in Whelp.")
-
-let uri_of_repr_kn ref (mp,dir,l) =
-  match mp with
-    | MPfile sl ->
-        uri_of_dirpath (Label.to_id l :: DirPath.repr dir @ DirPath.repr sl)
-    | _ ->
-        error_whelp_unknown_reference ref
-
-let url_paren f l = url_char '('; f l; url_char ')'
-let url_bracket f l = url_char '['; f l; url_char ']'
-
-let whelp_of_glob_sort = function
-  | GProp -> "Prop"
-  | GSet -> "Set"
-  | GType _ -> "Type"
-
-let uri_int n = Buffer.add_string b (string_of_int n)
-
-let uri_of_ind_pointer l =
-  url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l
-
-let uri_of_global ref =
-  match ref with
-  | VarRef id -> error ("Unknown Whelp reference: "^(Id.to_string id)^".")
-  | ConstRef cst ->
-      uri_of_repr_kn ref (repr_con cst); url_string ".con"
-  | IndRef (kn,i) ->
-      uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1]
-  | ConstructRef ((kn,i),j) ->
-      uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1;j]
-
-let whelm_special = Id.of_string "WHELM_ANON_VAR"
-
-let url_of_name = function
-  | Name id -> url_id id
-  | Anonymous -> url_id whelm_special (* No anon id in Whelp *)
-
-let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c
-
-let uri_params f = function
-  | [] -> ()
-  | l -> url_string "\\subst";
-         url_bracket (url_list_with_sep ";" (uri_of_binding f)) l
-
-let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
-
-let section_parameters = function
-  | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_)),_) ->
-      get_discharged_hyp_names (path_of_global (IndRef(induri,0)))
-  | GRef (_,(ConstRef cst as ref),_) ->
-      get_discharged_hyp_names (path_of_global ref)
-  | _ -> []
-
-let merge vl al =
-  let rec aux acc = function
-  | ([],l) | (_,([] as l)) -> List.rev acc, l
-  | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al)
-  in aux [] (vl,al)
-
-let rec uri_of_constr c =
-  match c with
-  | GVar (_,id) -> url_id id
-  | GRef (_,ref,_) ->  uri_of_global ref
-  | GHole _ | GEvar _ -> url_string "?"
-  | GSort (_,s) -> url_string (whelp_of_glob_sort s)
-  | GApp (_,f,args) ->
-      let inst,rest = merge (section_parameters f) args in
-      uri_of_constr f; url_char ' '; uri_params uri_of_constr inst;
-      url_list_with_sep " " uri_of_constr rest
-  | GLambda (_,na,k,ty,c) ->
-      url_string "\\lambda "; url_of_name na; url_string ":";
-      uri_of_constr ty; url_string "."; uri_of_constr c
-  | GProd (_,Anonymous,k,ty,c) ->
-      uri_of_constr ty; url_string "\\to "; uri_of_constr c
-  | GProd (_,Name id,k,ty,c) ->
-      url_string "\\forall "; url_id id; url_string ":";
-      uri_of_constr ty; url_string "."; uri_of_constr c
-  | GLetIn (_,na,b,c) ->
-      url_string "let "; url_of_name na; url_string "\\def ";
-      uri_of_constr b; url_string " in "; uri_of_constr c
-  | GCast (_,c, (CastConv t|CastVM t|CastNative t)) ->
-      uri_of_constr c; url_string ":"; uri_of_constr t
-  | GRec _ | GIf _ | GLetTuple _ | GCases _ ->
-      error "Whelp does not support pattern-matching and (co-)fixpoint."
-  | GCast (_,_, CastCoerce) ->
-      anomaly (Pp.str "Written w/o parenthesis")
-  | GPatVar _ ->
-      anomaly (Pp.str "Found constructors not supported in constr")
-
-let make_string f x = Buffer.reset b; f x; Buffer.contents b
-
-let send_whelp req s =
-  let url = make_whelp_request req s in
-  let command = Util.subst_command_placeholder browser_cmd_fmt url in
-  let _ = CUnix.run_command ~hook:print_string command in ()
-
-let whelp_constr env sigma req c =
-  let c = detype false [whelm_special] env sigma c in
-  send_whelp req (make_string uri_of_constr c)
-
-let whelp_constr_expr req c =
-  let (sigma,env)= Lemmas.get_current_context () in
-  let _,c = interp_open_constr env sigma c in
-  whelp_constr env sigma req c
-
-let whelp_locate s =
-  send_whelp "locate" s
-
-let whelp_elim ind =
-  send_whelp "elim" (make_string uri_of_global (IndRef ind))
-
-let on_goal f =
-  let gls = Proof.V82.subgoals (get_pftreestate ()) in
-  let gls = { gls with Evd.it = List.hd gls.Evd.it }  in
-  f (pf_env gls) (project gls) (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
-
-type whelp_request =
-  | Locate of string
-  | Elim of inductive
-  | Constr of string * constr
-
-let whelp = function
-  | Locate s -> whelp_locate s
-  | Elim ind -> whelp_elim ind
-  | Constr (s,c) -> whelp_constr (Global.env()) (Evd.empty) s c
-
-VERNAC ARGUMENT EXTEND whelp_constr_request
-| [ "Match" ] -> [ "match" ]
-| [ "Instance" ] -> [ "instance" ]
-END
-
-VERNAC COMMAND EXTEND Whelp CLASSIFIED AS QUERY
-| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ]
-| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ]
-| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ]
-| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
-END
-
-VERNAC COMMAND EXTEND WhelpHint CLASSIFIED AS QUERY
-| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ]
-| [ "Whelp" "Hint" ] => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] ->
-  [ on_goal (fun env sigma -> whelp_constr env sigma "hint") ]
-END
diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli
deleted file mode 100644
index 62272c50..00000000
--- a/toplevel/whelp.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Coq interface to the Whelp query engine developed at
-   the University of Bologna *)
-
-open Names
-open Term
-
-type whelp_request =
-  | Locate of string
-  | Elim of inductive
-  | Constr of string * constr
-
-val whelp : whelp_request -> unit