30 files changed, 546 insertions, 398 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index cc59a96834..f600432c80 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -193,48 +193,48 @@ let build_beq_scheme mode kn =
   let create_input c =
     let myArrow u v = mkArrow u Sorts.Relevant (lift 1 v)
     and eqName = function
-        | Name s -> Id.of_string ("eq_"^(Id.to_string s))
-        | Anonymous -> Id.of_string "eq_A"
+      | Name s -> Id.of_string ("eq_"^(Id.to_string s))
+      | Anonymous -> Id.of_string "eq_A"
     in
     let ext_rel_list = Context.Rel.to_extended_list mkRel 0 lnamesparrec in
-      let lift_cnt = ref 0 in
-      let eqs_typ = List.map (fun aa ->
-                                let a = lift !lift_cnt aa in
-                                  incr lift_cnt;
-                                  myArrow a (myArrow a (bb ()))
-                             ) ext_rel_list in
-
-        let eq_input = List.fold_left2
-          ( fun a b decl -> (* mkLambda(n,b,a) ) *)
-                (* here I leave the Naming thingy so that the type of
+    let lift_cnt = ref 0 in
+    let eqs_typ = List.map (fun aa ->
+                      let a = lift !lift_cnt aa in
+                      incr lift_cnt;
+                      myArrow a (myArrow a (bb ()))
+                    ) ext_rel_list in
+
+    let eq_input = List.fold_left2
+                     ( fun a b decl -> (* mkLambda(n,b,a) ) *)
+                       (* here I leave the Naming thingy so that the type of
                   the function is more readable for the user *)
-                mkNamedLambda (map_annot eqName (RelDecl.get_annot decl)) b a )
-                c (List.rev eqs_typ) lnamesparrec
-       in
-        List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *)
-           (* Same here , hoping the auto renaming will do something good ;)  *)
-           let x = map_annot
-               (function Name s -> s | Anonymous -> Id.of_string "A")
-               (RelDecl.get_annot decl)
-           in
-          mkNamedLambda x (RelDecl.get_type decl)  a) eq_input lnamesparrec
- in
- let make_one_eq cur =
-  let u = Univ.Instance.empty in
-  let ind = (kn,cur),u (* FIXME *) in
-  (* current inductive we are working on *)
-  let cur_packet = mib.mind_packets.(snd (fst ind)) in
-  (* Inductive toto : [rettyp] := *)
-  let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in
-  (* split rettyp in a list without the non rec params and the last ->
+                       mkNamedLambda (map_annot eqName (RelDecl.get_annot decl)) b a )
+                     c (List.rev eqs_typ) lnamesparrec
+    in
+    List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *)
+        (* Same here , hoping the auto renaming will do something good ;)  *)
+        let x = map_annot
+                  (function Name s -> s | Anonymous -> Id.of_string "A")
+                  (RelDecl.get_annot decl)
+        in
+        mkNamedLambda x (RelDecl.get_type decl)  a) eq_input lnamesparrec
+  in
+  let make_one_eq cur =
+    let u = Univ.Instance.empty in
+    let ind = (kn,cur),u (* FIXME *) in
+    (* current inductive we are working on *)
+    let cur_packet = mib.mind_packets.(snd (fst ind)) in
+    (* Inductive toto : [rettyp] := *)
+    let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in
+    (* split rettyp in a list without the non rec params and the last ->
   e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *)
-  let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in
+    let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in
     (* give a type A, this function tries to find the equality on A declared
        previously *)
     (*  nlist = the number of args (A , B , ... )
         eqA   = the de Bruijn index of the first eq param
         ndx   = how much to translate due to the 2nd Case
-    *)
+     *)
     let compute_A_equality rel_list nlist eqA ndx t =
       let lifti = ndx in
       let rec aux c =
@@ -243,47 +243,47 @@ let build_beq_scheme mode kn =
         match Constr.kind c with
         | Rel x -> mkRel (x-nlist+ndx)
         | Var x ->
-          (* Support for working in a context with "eq_x : x -> x -> bool" *)
-          let eid = Id.of_string ("eq_"^(Id.to_string x)) in
-          let () =
-            try ignore (Environ.lookup_named eid env)
-            with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x))
-          in
-          mkVar eid
+           (* Support for working in a context with "eq_x : x -> x -> bool" *)
+           let eid = Id.of_string ("eq_"^(Id.to_string x)) in
+           let () =
+             try ignore (Environ.lookup_named eid env)
+             with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x))
+           in
+           mkVar eid
         | Cast (x,_,_) -> aux (Term.applist (x,a))
         | App _ -> assert false
         | Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
-            if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
-            else begin
-              try
-                let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with
-                | Some c -> mkConst c
-                | None -> assert false
-                in
-                let eqa = Array.of_list @@ List.map aux a in
-                let args =
-                  Array.append
-                    (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
-                if Int.equal (Array.length args) 0 then eq
-                else mkApp (eq, args)
-              with Not_found -> raise(EqNotFound (ind', fst ind))
-            end
+           if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
+           else begin
+               try
+                 let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with
+                   | Some c -> mkConst c
+                   | None -> assert false
+                 in
+                 let eqa = Array.of_list @@ List.map aux a in
+                 let args =
+                   Array.append
+                     (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
+                 if Int.equal (Array.length args) 0 then eq
+                 else mkApp (eq, args)
+               with Not_found -> raise(EqNotFound (ind', fst ind))
+             end
         | Sort _  -> raise InductiveWithSort
         | Prod _ -> raise InductiveWithProduct
         | Lambda _-> raise (EqUnknown "abstraction")
         | LetIn _ -> raise (EqUnknown "let-in")
         | Const (kn, u) ->
-             (match Environ.constant_opt_value_in env (kn, u) with
-              | Some c -> aux (Term.applist (c,a))
-              | None ->
-                 (* Support for working in a context with "eq_x : x -> x -> bool" *)
-                 (* Needs Hints, see test suite *)
-                 let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in
-                 let kneq = Constant.change_label kn eq_lbl in
-                 if Environ.mem_constant kneq env then
-                   let _ = Environ.constant_opt_value_in env (kneq, u) in
-                   Term.applist (mkConst kneq,a)
-                 else raise (ParameterWithoutEquality (GlobRef.ConstRef kn)))
+           (match Environ.constant_opt_value_in env (kn, u) with
+            | Some c -> aux (Term.applist (c,a))
+            | None ->
+               (* Support for working in a context with "eq_x : x -> x -> bool" *)
+               (* Needs Hints, see test suite *)
+               let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in
+               let kneq = Constant.change_label kn eq_lbl in
+               if Environ.mem_constant kneq env then
+                 let _ = Environ.constant_opt_value_in env (kneq, u) in
+                 Term.applist (mkConst kneq,a)
+               else raise (ParameterWithoutEquality (GlobRef.ConstRef kn)))
         | Proj _ -> raise (EqUnknown "projection")
         | Construct _ -> raise (EqUnknown "constructor")
         | Case _ -> raise (EqUnknown "match")
@@ -293,100 +293,112 @@ let build_beq_scheme mode kn =
         | Evar _  -> raise (EqUnknown "existential variable")
         | Int _ -> raise (EqUnknown "int")
         | Float _ -> raise (EqUnknown "float")
-              | Array _ -> raise (EqUnknown "array")
-    in
+        | Array _ -> raise (EqUnknown "array")
+      in
       aux t
-  in
-  (* construct the predicate for the Case part*)
-  let do_predicate rel_list n =
-     List.fold_left (fun a b -> mkLambda(make_annot Anonymous Sorts.Relevant,b,a))
-      (mkLambda (make_annot Anonymous Sorts.Relevant,
-                 mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
-                 (bb ())))
-      (List.rev rettyp_l) in
-  (* make_one_eq *)
-  (* do the [| C1 ... =>  match Y with ... end
+    in
+    (* construct the predicate for the Case part*)
+    let do_predicate rel_list n =
+      List.fold_left (fun a b -> mkLambda(make_annot Anonymous Sorts.Relevant,b,a))
+        (mkLambda (make_annot Anonymous Sorts.Relevant,
+                   mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
+                   (bb ())))
+        (List.rev rettyp_l) in
+    (* make_one_eq *)
+    (* do the [| C1 ... =>  match Y with ... end
                ...
                Cn => match Y with ... end |]  part *)
     let rci = Sorts.Relevant in (* TODO relevance *)
     let ci = make_case_info env (fst ind) rci MatchStyle in
-    let constrs n = get_constructors env (make_ind_family (ind,
-      Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in
+    let constrs n =
+      let params = Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt in
+      get_constructors env (make_ind_family (ind, params))
+    in
     let constrsi = constrs (3+nparrec) in
     let n = Array.length constrsi in
-    let ar = Array.make n (ff ()) in
-        for i=0 to n-1 do
-          let nb_cstr_args = List.length constrsi.(i).cs_args in
-          let ar2 = Array.make n (ff ()) in
-          let constrsj = constrs (3+nparrec+nb_cstr_args) in
-            for j=0 to n-1 do
-              if Int.equal i j then
-                ar2.(j) <- let cc = (match nb_cstr_args with
-                    | 0 -> tt ()
-                    | _ -> let eqs = Array.make nb_cstr_args (tt ()) in
-                      for ndx = 0 to nb_cstr_args-1 do
-                        let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in
-                          let eqA = compute_A_equality rel_list
-                                          nparrec
-                                          (nparrec+3+2*nb_cstr_args)
-                                          (nb_cstr_args+ndx+1)
-                                          cc
-                          in
-                          Array.set eqs ndx
-                              (mkApp (eqA,
-                                [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
-                              ))
-                      done;
-                      Array.fold_left
-                          (fun a b -> mkApp (andb(),[|b;a|]))
-                          (eqs.(0))
-                          (Array.sub eqs 1 (nb_cstr_args - 1))
-                  )
-                  in
-                    (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) cc
-                    (constrsj.(j).cs_args)
-                )
-              else ar2.(j) <- (List.fold_left (fun a decl ->
-                        mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) (ff ())  (constrsj.(j).cs_args) )
-            done;
-
-          ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
-                        (mkCase (Inductive.contract_case env ((ci,do_predicate rel_list nb_cstr_args,
-                                  NoInvert, mkVar (Id.of_string "Y") ,ar2))))
-                         (constrsi.(i).cs_args))
-        done;
-        mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1))  (
-          mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2))  (
-            mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar))))
-    in (* build_beq_scheme *)
-    let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
-        types = Array.make nb_ind mkSet and
-        cores = Array.make nb_ind mkSet in
-    let u = Univ.Instance.empty in
-    for i=0 to (nb_ind-1) do
-        names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant;
-        types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant
-                     (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ()));
-        let c = make_one_eq i in
-        cores.(i) <- c;
-    done;
-      (Array.init nb_ind (fun i ->
-      let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
-        if not (Sorts.family_leq InSet kelim) then
-          raise (NonSingletonProp (kn,i));
-        let fix = match mib.mind_finite with
-        | CoFinite ->
-          raise NoDecidabilityCoInductive;
-        | Finite ->
-          mkFix (((Array.make nb_ind 0),i),(names,types,cores))
-        | BiFinite ->
-          (* If the inductive type is not recursive, the fixpoint is
+    let ar = Array.init n (fun i ->
+      let nb_cstr_args = List.length constrsi.(i).cs_args in
+      let constrsj = constrs (3+nparrec+nb_cstr_args) in
+      let ar2 = Array.init n (fun j ->
+        if Int.equal i j then
+          let cc = match nb_cstr_args with
+            | 0 -> tt ()
+            | _ ->
+               let eqs = Array.init nb_cstr_args (fun ndx ->
+                 let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in
+                 let eqA = compute_A_equality rel_list
+                             nparrec
+                             (nparrec+3+2*nb_cstr_args)
+                             (nb_cstr_args+ndx+1)
+                             cc
+                 in
+                 mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]))
+               in
+               Array.fold_left
+                 (fun a b -> mkApp (andb(),[|b;a|]))
+                 eqs.(0)
+                 (Array.sub eqs 1 (nb_cstr_args - 1))
+          in
+          List.fold_left (fun a decl ->
+              mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
+            cc
+            constrsj.(j).cs_args
+        else
+          List.fold_left (fun a decl ->
+              mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
+            (ff ())
+            (constrsj.(j).cs_args))
+      in
+      let pred = EConstr.of_constr (do_predicate rel_list nb_cstr_args) in
+      let case =
+        simple_make_case_or_project env (Evd.from_env env)
+          ci pred NoInvert (EConstr.mkVar (Id.of_string "Y"))
+          (EConstr.of_constr_array ar2)
+      in
+      List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
+        (EConstr.Unsafe.to_constr case)
+        (constrsi.(i).cs_args))
+    in
+    let pred = EConstr.of_constr (do_predicate rel_list 0) in
+    let case =
+      simple_make_case_or_project env (Evd.from_env env)
+        ci pred NoInvert (EConstr.mkVar (Id.of_string "X"))
+        (EConstr.of_constr_array ar)
+    in
+    mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1))  (
+        mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2))  (
+            (EConstr.Unsafe.to_constr case)))
+  in (* build_beq_scheme *)
+
+  let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
+      types = Array.make nb_ind mkSet and
+      cores = Array.make nb_ind mkSet in
+  let u = Univ.Instance.empty in
+  for i=0 to (nb_ind-1) do
+    names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant;
+    types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant
+                  (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ()));
+    let c = make_one_eq i in
+    cores.(i) <- c;
+  done;
+  let res = Array.init nb_ind (fun i ->
+    let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
+    if not (Sorts.family_leq InSet kelim) then
+      raise (NonSingletonProp (kn,i));
+    let fix = match mib.mind_finite with
+      | CoFinite ->
+         raise NoDecidabilityCoInductive;
+      | Finite ->
+         mkFix (((Array.make nb_ind 0),i),(names,types,cores))
+      | BiFinite ->
+         (* If the inductive type is not recursive, the fixpoint is
              not used, so let's replace it with garbage *)
-          let subst = List.init nb_ind (fun _ -> mkProp) in
-          Vars.substl subst cores.(i)
-        in
-        create_input fix),
-       UState.from_env (Global.env ()))
+         let subst = List.init nb_ind (fun _ -> mkProp) in
+         Vars.substl subst cores.(i)
+    in
+    create_input fix)
+  in
+  res, UState.from_env (Global.env ())
 
 let beq_scheme_kind =
   declare_mutual_scheme_object "_beq"
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 15d8ebc4b5..86b15739f9 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -237,24 +237,24 @@ let open_coercion i o =
     cache_coercion o
 
 let discharge_coercion (_, c) =
-  if c.coercion_local then None
+  if c.coe_local then None
   else
     let n =
       try
-        let ins = Lib.section_instance c.coercion_type in
+        let ins = Lib.section_instance c.coe_value in
         Array.length (snd ins)
       with Not_found -> 0
     in
     let nc = { c with
-      coercion_params = n + c.coercion_params;
-      coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
+      coe_param = n + c.coe_param;
+      coe_is_projection = Option.map Lib.discharge_proj_repr c.coe_is_projection;
     } in
     Some nc
 
 let classify_coercion obj =
-  if obj.coercion_local then Dispose else Substitute obj
+  if obj.coe_local then Dispose else Substitute obj
 
-let inCoercion : coercion -> obj =
+let inCoercion : coe_info_typ -> obj =
   declare_object {(default_object "COERCION") with
     open_function = simple_open open_coercion;
     cache_function = cache_coercion;
@@ -269,13 +269,13 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps
     | _ -> None
   in
   let c = {
-    coercion_type = coef;
-    coercion_local = local;
-    coercion_is_id = isid;
-    coercion_is_proj = isproj;
-    coercion_source = cls;
-    coercion_target = clt;
-    coercion_params = ps;
+    coe_value = coef;
+    coe_local = local;
+    coe_is_identity = isid;
+    coe_is_projection = isproj;
+    coe_source = cls;
+    coe_target = clt;
+    coe_param = ps;
   } in
   Lib.add_anonymous_leaf (inCoercion c)
 
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b3ffb864f2..2e48313630 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -111,6 +111,10 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
   evd, (c, tyopt), imps
 
+let definition_using env evd ~body ~types ~using =
+  let terms = Option.List.cons types [body] in
+  Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using
+
 let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = false in
   let env = Global.env() in
@@ -120,11 +124,7 @@ let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl r
   let evd, (body, types), impargs =
     interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
-  let using = using |> Option.map (fun expr ->
-    let terms = body :: match types with Some x -> [x] | None -> [] in
-    let l = Proof_using.process_expr (Global.env()) evd expr terms in
-    Names.Id.Set.(List.fold_right add l empty))
-  in
+  let using = definition_using env evd ~body ~types ~using in
   let kind = Decls.IsDefinition kind in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
   let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly ?typing_flags () in
@@ -141,11 +141,7 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ?typing_flags ~kind ?usin
   let evd, (body, types), impargs =
     interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
-  let using = using |> Option.map (fun expr ->
-    let terms = body :: match types with Some x -> [x] | None -> [] in
-    let l = Proof_using.process_expr (Global.env()) evd expr terms in
-    Names.Id.Set.(List.fold_right add l empty))
-  in
+  let using = definition_using env evd ~body ~types ~using in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
     let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0cf0b07822..0f817ffbd1 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -259,13 +259,10 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps =
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        let using = using |> Option.map (fun expr ->
-          let terms = [EConstr.of_constr typ] in
-          let env = Global.env() in
-          let sigma = Evd.from_env env in
-          let l = Proof_using.process_expr env sigma expr terms in
-          Names.Id.Set.(List.fold_right add l empty))
-        in
+        let env = Global.env() in
+        let evd = Evd.from_env env in
+        let terms = [EConstr.of_constr typ] in
+        let using = Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using in
         let args = List.map Context.Rel.Declaration.get_name ctx in
         Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
       ) fixnames fixtypes fiximps
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3c4a651cf5..0651f3330e 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -259,10 +259,9 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?typing_flags ?using r
   let evars, _, evars_def, evars_typ =
     RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
-  let using = using |> Option.map (fun expr ->
+  let using =
     let terms = List.map EConstr.of_constr [evars_def; evars_typ] in
-    let l = Proof_using.process_expr env sigma expr terms in
-    Names.Id.Set.(List.fold_right add l empty))
+    Option.map (fun using -> Proof_using.definition_using env sigma ~using ~terms) using
   in
   let uctx = Evd.evar_universe_context sigma in
   let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
@@ -294,11 +293,8 @@ let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind fixl =
   let evd = nf_evar_map_undefined evd in
   let collect_evars name def typ impargs =
     (* Generalize by the recursive prototypes  *)
-    let using = using |> Option.map (fun expr ->
-      let terms = [def; typ] in
-      let l = Proof_using.process_expr env evd expr terms in
-      Names.Id.Set.(List.fold_right add l empty))
-    in
+    let terms = [def; typ] in
+    let using = Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using in
     let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index af51f4fafb..1b811f3db7 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -105,12 +105,6 @@ let () =
       optread  = (fun () -> !search_output_name_only);
       optwrite = (:=) search_output_name_only }
 
-let deprecated_searchhead =
-  CWarnings.create
-    ~name:"deprecated-searchhead"
-    ~category:"deprecated"
-    (fun () -> Pp.str("SearchHead is deprecated. Use the headconcl: clause of Search instead."))
-
 let interp_search env sigma s r =
   let r = interp_search_restriction r in
   let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in
@@ -138,9 +132,6 @@ let interp_search env sigma s r =
       (Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchRewrite c ->
       (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
-  | SearchHead c ->
-      deprecated_searchhead ();
-      (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
   | Search sl ->
       (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |>
        Search.prioritize_search) pr_search);
diff --git a/vernac/declare.ml b/vernac/declare.ml
index c715304419..607ba18a95 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -57,7 +57,7 @@ module CInfo = struct
     (** Names to pre-introduce  *)
     ; impargs : Impargs.manual_implicits
     (** Explicitily declared implicit arguments  *)
-    ; using : Names.Id.Set.t option
+    ; using : Proof_using.t option
     (** Explicit declaration of section variables used by the constant *)
     }
 
@@ -889,13 +889,6 @@ let add_hint local prg cst =
   let locality = if local then Goptions.OptLocal else Goptions.OptExport in
   Hints.add_hints ~locality [Id.to_string prg.prg_cinfo.CInfo.name] (unfold_entry cst)
 
-(* true = hide obligations *)
-let get_hide_obligations =
-  Goptions.declare_bool_option_and_ref
-    ~depr:true
-    ~key:["Hide"; "Obligations"]
-    ~value:false
-
 let declare_obligation prg obl ~uctx ~types ~body =
   let poly = prg.prg_info.Info.poly in
   let univs = UState.univ_entry ~poly uctx in
@@ -1046,51 +1039,10 @@ let obligation_substitution expand prg =
   let ints = intset_to (pred (Array.length obls)) in
   obl_substitution expand obls ints
 
-let hide_obligation () =
-  Coqlib.check_required_library ["Coq"; "Program"; "Tactics"];
-  UnivGen.constr_of_monomorphic_global
-    (Coqlib.lib_ref "program.tactics.obligation")
-
-(* XXX: Is this the right place? *)
-let rec prod_app t n =
-  match
-    Constr.kind
-      (EConstr.Unsafe.to_constr
-         (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t)))
-    (* FIXME *)
-  with
-  | Prod (_, _, b) -> Vars.subst1 n b
-  | LetIn (_, b, t, b') -> prod_app (Vars.subst1 b b') n
-  | _ ->
-    CErrors.user_err ~hdr:"prod_app"
-      Pp.(str "Needed a product, but didn't find one" ++ fnl ())
-
-(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_applist t nL = List.fold_left prod_app t nL
-
-let replace_appvars subst =
-  let rec aux c =
-    let f, l = decompose_app c in
-    if isVar f then
-      try
-        let c' = List.map (Constr.map aux) l in
-        let t, b = Id.List.assoc (destVar f) subst in
-        mkApp
-          ( delayed_force hide_obligation
-          , [|prod_applist t c'; Term.applistc b c'|] )
-      with Not_found -> Constr.map aux c
-    else Constr.map aux c
-  in
-  Constr.map aux
-
 let subst_prog subst prg =
-  if get_hide_obligations () then
-    ( replace_appvars subst prg.prg_body
-    , replace_appvars subst (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
-  else
-    let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
-    ( Vars.replace_vars subst' prg.prg_body
-    , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
+  let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
+  ( Vars.replace_vars subst' prg.prg_body
+  , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_cinfo.CInfo.typ )
 
 let declare_definition ~pm prg =
   let varsubst = obligation_substitution true prg in
@@ -1526,11 +1478,10 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl =
 let get_used_variables pf = pf.using
 let get_universe_decl pf = pf.pinfo.Proof_info.info.Info.udecl
 
-let set_used_variables ps l =
+let set_used_variables ps ~using =
   let open Context.Named.Declaration in
   let env = Global.env () in
-  let ids = List.fold_right Id.Set.add l Id.Set.empty in
-  let ctx = Environ.keep_hyps env ids in
+  let ctx = Environ.keep_hyps env using in
   let ctx_set =
     List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
   let vars_of = Environ.global_vars_set in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 37a61cc4f0..81558e6f6b 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -79,7 +79,7 @@ module CInfo : sig
     -> typ:'constr
     -> ?args:Name.t list
     -> ?impargs:Impargs.manual_implicits
-    -> ?using:Names.Id.Set.t
+    -> ?using:Proof_using.t
     -> unit
     -> 'constr t
 
@@ -244,7 +244,7 @@ module Proof : sig
 
   (** Sets the section variables assumed by the proof, returns its closure
    * (w.r.t. type dependencies and let-ins covered by it) *)
-  val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t
+  val set_used_variables : t -> using:Proof_using.t -> Constr.named_context * t
 
   (** Gets the set of variables declared to be used by the proof. None means
       no "Proof using" or #[using] was given *)
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 834ef0d29a..91ab17575d 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -74,6 +74,10 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
       subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
 
+let input_univ_names (src, l) =
+  if CList.is_empty l then ()
+  else Lib.add_anonymous_leaf (input_univ_names (src, l))
+
 let invent_name (named,cnt) u =
   let rec aux i =
     let na = Id.of_string ("u"^(string_of_int i)) in
@@ -120,7 +124,7 @@ let declare_univ_binders gr pl =
         aux, (id,univ) :: univs)
         (LSet.diff levels named) ((pl,0),univs)
     in
-    Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
+    input_univ_names (QualifiedUniv l, univs)
 
 let do_universe ~poly l =
   let in_section = Global.sections_are_opened () in
@@ -134,7 +138,7 @@ let do_universe ~poly l =
       Univ.LSet.empty l, Univ.Constraint.empty
   in
   let src = if poly then BoundUniv else UnqualifiedUniv in
-  let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
+  let () = input_univ_names (src, l) in
   DeclareUctx.declare_universe_context ~poly ctx
 
 let do_constraint ~poly l =
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index d2eeebc246..15e6d4ef37 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -301,7 +301,10 @@ and load_keep i ((sp,kn),kobjs) =
 let mark_object f obj (exports,acc) =
   (exports, (f,obj)::acc)
 
-let rec collect_module_objects (f,mp) acc =
+let rec collect_modules mpl acc =
+  List.fold_left (fun acc fmp -> collect_module fmp acc) acc (List.rev mpl)
+
+and collect_module (f,mp) acc =
   (* May raise Not_found for unknown module and for functors *)
   let modobjs = ModObjs.get mp in
   let prefix = modobjs.module_prefix in
@@ -310,14 +313,16 @@ let rec collect_module_objects (f,mp) acc =
 
 and collect_object f i (name, obj as o) acc =
   match obj with
-  | ExportObject { mpl } -> collect_export f i mpl acc
+  | ExportObject { mpl } -> collect_exports f i mpl acc
   | AtomicObject _ | IncludeObject _ | KeepObject _
   | ModuleObject _ | ModuleTypeObject _ -> mark_object f o acc
 
 and collect_objects f i prefix objs acc =
-  List.fold_right (fun (id, obj) acc -> collect_object f i (Lib.make_oname prefix id, obj) acc) objs acc
+  List.fold_left (fun acc (id, obj) ->
+    collect_object f i (Lib.make_oname prefix id, obj) acc
+  ) acc (List.rev objs)
 
-and collect_one_export f (f',mp) (exports,objs as acc) =
+and collect_export f (f',mp) (exports,objs as acc) =
   match filter_and f f' with
   | None -> acc
   | Some f ->
@@ -334,12 +339,12 @@ and collect_one_export f (f',mp) (exports,objs as acc) =
     *)
     if exports == exports' then acc
     else
-      collect_module_objects (f,mp) (exports', objs)
+      collect_module (f,mp) (exports', objs)
 
 
-and collect_export f i mpl acc =
+and collect_exports f i mpl acc =
   if Int.equal i 1 then
-    List.fold_right (collect_one_export f) mpl acc
+    List.fold_left (fun acc fmp -> collect_export f fmp acc) acc (List.rev mpl)
   else acc
 
 let open_modtype i ((sp,kn),_) =
@@ -388,7 +393,7 @@ and open_include f i ((sp,kn), aobjs) =
   open_objects f i prefix o
 
 and open_export f i mpl =
-  let _,objs = collect_export f i mpl (MPmap.empty, []) in
+  let _,objs = collect_exports f i mpl (MPmap.empty, []) in
   List.iter (fun (f,o) -> open_object f 1 o) objs
 
 and open_keep f i ((sp,kn),kobjs) =
@@ -1056,7 +1061,7 @@ let end_library ?except ~output_native_objects dir =
   cenv,(substitute,keep),ast
 
 let import_modules ~export mpl =
-  let _,objs = List.fold_right collect_module_objects mpl (MPmap.empty, []) in
+  let _,objs = collect_modules mpl (MPmap.empty, []) in
   List.iter (fun (f,o) -> open_object f 1 o) objs;
   if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
 
diff --git a/vernac/dune b/vernac/dune
index ba361b1377..7319b1353c 100644
--- a/vernac/dune
+++ b/vernac/dune
@@ -1,7 +1,7 @@
 (library
  (name vernac)
  (synopsis "Coq's Vernacular Language")
- (public_name coq.vernac)
+ (public_name coq-core.vernac)
  (wrapped false)
  (libraries tactics parsing))
 
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5c329f60a9..f8a28332b1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -965,8 +965,6 @@ GRAMMAR EXTEND Gram
       (* Searching the environment *)
       | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." ->
          { fun g -> VernacPrint (PrintAbout (qid,l,g)) }
-      | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." ->
-          { fun g -> VernacSearch (SearchHead c,g, l) }
       | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
           { fun g -> VernacSearch (SearchPattern c,g, l) }
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
diff --git a/vernac/library.ml b/vernac/library.ml
index 8a9b1fd68d..cc9e3c3c44 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -155,17 +155,13 @@ let library_is_loaded dir =
 
 let register_loaded_library m =
   let libname = m.libsum_name in
-  let link () =
-    let dirname = Filename.dirname (library_full_filename libname) in
-    let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
-    let f = prefix ^ "cmo" in
-    let f = Dynlink.adapt_filename f in
-    Nativelib.link_library ~prefix ~dirname ~basename:f
-  in
   let rec aux = function
     | [] ->
-      let () = if Flags.get_native_compiler () then link () in
-      [libname]
+        if Flags.get_native_compiler () then begin
+            let dirname = Filename.dirname (library_full_filename libname) in
+            Nativelib.enable_library dirname libname
+          end;
+        [libname]
     | m'::_ as l when DirPath.equal m' libname -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e6244ee3b5..2fe402ff08 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1793,15 +1793,9 @@ let remove_delimiters local scope =
 let add_class_scope local scope cl =
   Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
 
-(* Check if abbreviation to a name and avoid early insertion of
-   maximal implicit arguments *)
-let try_interp_name_alias = function
-  | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
-  | _ -> raise Not_found
-
 let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
   let acvars,pat,reversibility =
-    try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible
+    try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible
     with Not_found ->
       let fold accu id = Id.Map.add id NtnInternTypeAny accu in
       let i_vars = List.fold_left fold Id.Map.empty vars in
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index ff4365c8d3..8e5942440b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -242,7 +242,6 @@ let pr_search a gopt b pr_p =
   pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
   ++
   match a with
-  | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | Search sl ->
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 0fc6c7f87b..ec6e3b44ba 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -947,7 +947,7 @@ let print_about_any ?loc env sigma k udecl =
   [hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
     let () = match Syntax_def.search_syntactic_definition kn with
-    | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
+    | [],Notation_term.NRef (ref,_) -> Dumpglob.add_glob ?loc ref
     | _ -> () in
       v 0 (
       print_syntactic_def env kn ++ fnl () ++
@@ -976,15 +976,11 @@ open Coercionops
 
 let print_coercion_value v = Printer.pr_global v.coe_value
 
-let print_class i =
-  let cl,_ = class_info_from_index i in
-  pr_class cl
-
 let print_path ((i,j),p) =
   hov 2 (
     str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
     str"] : ") ++
-  print_class i ++ str" >-> " ++ print_class j
+  pr_class i ++ str" >-> " ++ pr_class j
 
 let _ = Coercionops.install_path_printer print_path
 
@@ -997,25 +993,16 @@ let print_classes () =
 let print_coercions () =
   pr_sequence print_coercion_value (coercions())
 
-let index_of_class cl =
-  try
-    fst (class_info cl)
-  with Not_found ->
-    user_err ~hdr:"index_of_class"
-      (pr_class cl ++ spc() ++ str "not a defined class.")
-
 let print_path_between cls clt =
-  let i = index_of_class cls in
-  let j = index_of_class clt in
   let p =
     try
-      lookup_path_between_class (i,j)
+      lookup_path_between_class (cls, clt)
     with Not_found ->
       user_err ~hdr:"index_cl_of_id"
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
          ++ str ".")
   in
-  print_path ((i,j),p)
+  print_path ((cls, clt), p)
 
 let print_canonical_projections env sigma grefs =
   let match_proj_gref ((x,y),c) gr =
diff --git a/vernac/printmod.ml b/vernac/printmod.ml
index fdf7f6c74a..ba4a7857e7 100644
--- a/vernac/printmod.ml
+++ b/vernac/printmod.ml
@@ -124,7 +124,7 @@ let print_mutual_inductive env mind mib udecl =
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (def keyword ++ spc () ++
          prlist_with_sep (fun () -> fnl () ++ str"  with ")
-           (print_one_inductive env sigma mib) inds ++
+           (print_one_inductive env sigma mib) inds ++ str "." ++
          Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes)
 
 let get_fields =
@@ -173,7 +173,7 @@ let print_record env mind mib udecl =
       prlist_with_sep (fun () -> str ";" ++ brk(2,0))
         (fun (id,b,c) ->
           Id.print id ++ str (if b then " : " else " := ") ++
-          Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
+          Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }." ++
     Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes
   )
 
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index bdb0cabacf..01e7b7cc3d 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -64,6 +64,12 @@ let process_expr env sigma e ty =
   let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in
   Id.Set.elements s
 
+type t = Names.Id.Set.t
+
+let definition_using env evd ~using ~terms =
+  let l = process_expr env evd using terms in
+  Names.Id.Set.(List.fold_right add l empty)
+
 let name_set id expr = known_names := (id,expr) :: !known_names
 
 let minimize_hyps env ids =
@@ -91,13 +97,14 @@ let remove_ids_and_lets env s ids =
 let record_proof_using expr =
   Aux_file.record_in_aux "suggest_proof_using" expr
 
+let debug_proof_using = CDebug.create ~name:"proof-using" ()
+
 (* Variables in [skip] come from after the definition, so don't count
    for "All". Used in the variable case since the env contains the
    variable itself. *)
 let suggest_common env ppid used ids_typ skip =
   let module S = Id.Set in
   let open Pp in
-  let print x = Feedback.msg_debug x in
   let pr_set parens s =
     let wrap ppcmds =
       if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
@@ -111,13 +118,13 @@ let suggest_common env ppid used ids_typ skip =
   in
   let all = S.diff all skip in
   let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in
-  if !Flags.debug then begin
-    print (str "All "        ++ pr_set false all);
-    print (str "Type "       ++ pr_set false ids_typ);
-    print (str "needed "     ++ pr_set false needed);
-    print (str "all_needed " ++ pr_set false all_needed);
-    print (str "Type* "      ++ pr_set false fwd_typ);
-  end;
+  let () = debug_proof_using (fun () ->
+      str "All "        ++ pr_set false all ++ fnl() ++
+      str "Type "       ++ pr_set false ids_typ ++ fnl() ++
+      str "needed "     ++ pr_set false needed ++ fnl() ++
+      str "all_needed " ++ pr_set false all_needed ++ fnl() ++
+      str "Type* "      ++ pr_set false fwd_typ)
+  in
   let valid_exprs = ref [] in
   let valid e = valid_exprs := e :: !valid_exprs in
   if S.is_empty needed then valid (str "Type");
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index 93dbd33ae4..60db4d60e6 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -10,10 +10,17 @@
 
 (** Utility code for section variables handling in Proof using... *)
 
-val process_expr :
-  Environ.env -> Evd.evar_map ->
-  Vernacexpr.section_subset_expr -> EConstr.types list ->
-    Names.Id.t list
+(** At some point it would be good to make this abstract *)
+type t = Names.Id.Set.t
+
+(** Process a [using] expression in definitions to provide the list of
+    used terms *)
+val definition_using
+  : Environ.env
+  -> Evd.evar_map
+  -> using:Vernacexpr.section_subset_expr
+  -> terms:EConstr.constr list
+  -> t
 
 val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
 
diff --git a/vernac/search.ml b/vernac/search.ml
index 501e5b1a91..98e231de19 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -185,14 +185,6 @@ let rec pattern_filter pat ref env sigma typ =
   | LetIn (_, _, _, typ) -> pattern_filter pat ref env sigma typ
   | _ -> false
 
-let rec head_filter pat ref env sigma typ =
-  let typ = Termops.strip_outer_cast sigma typ in
-  if Constr_matching.is_matching_head env sigma pat typ then true
-  else match EConstr.kind sigma typ with
-  | Prod (_, _, typ)
-  | LetIn (_, _, _, typ) -> head_filter pat ref env sigma typ
-  | _ -> false
-
 let full_name_of_reference ref =
   let (dir,id) = repr_path (Nametab.path_of_global ref) in
   DirPath.to_string dir ^ "." ^ Id.to_string id
@@ -274,19 +266,6 @@ let search_rewrite env sigma pat mods pr_search =
 
 (** Search *)
 
-let search_by_head env sigma pat mods pr_search =
-  let filter ref kind env typ =
-    module_filter mods ref kind env sigma typ &&
-    head_filter pat ref env sigma (EConstr.of_constr typ) &&
-    blacklist_filter ref kind env sigma typ
-  in
-  let iter ref kind env typ =
-    if filter ref kind env typ then pr_search ref kind env typ
-  in
-  generic_search env iter
-
-(** Search *)
-
 let search env sigma items mods pr_search =
   let filter ref kind env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
diff --git a/vernac/search.mli b/vernac/search.mli
index 09847f4e03..6557aa5986 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -47,8 +47,6 @@ val search_filter : glob_search_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
-                  -> display_function -> unit
 val search_rewrite : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
 val search_pattern : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index cd0dd5e9a6..007a3b05fc 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -45,3 +45,4 @@ ComArguments
 Vernacentries
 ComTactic
 Vernacinterp
+Vernac_classifier
diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml
new file mode 100644
index 0000000000..ffae2866c0
--- /dev/null
+++ b/vernac/vernac_classifier.ml
@@ -0,0 +1,215 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open CErrors
+open Util
+open Pp
+open CAst
+open Vernacextend
+open Vernacexpr
+
+let string_of_vernac_when = function
+  | VtLater -> "Later"
+  | VtNow -> "Now"
+
+let string_of_vernac_classification = function
+  | VtStartProof _ -> "StartProof"
+  | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w)
+  | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
+  | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)"
+  | VtQed VtDrop -> "Qed(drop)"
+  | VtProofStep {  proof_block_detection } ->
+      "ProofStep " ^ Option.default "" proof_block_detection
+  | VtQuery -> "Query"
+  | VtMeta -> "Meta "
+  | VtProofMode _ -> "Proof Mode"
+
+let vtkeep_of_opaque = function
+  | Opaque -> VtKeepOpaque
+  | Transparent -> VtKeepDefined
+
+let idents_of_name : Names.Name.t -> Names.Id.t list =
+  function
+  | Names.Anonymous -> []
+  | Names.Name n -> [n]
+
+let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
+
+let options_affecting_stm_scheduling =
+  [ Attributes.universe_polymorphism_option_name;
+    stm_allow_nested_proofs_option_name;
+    Vernacinterp.proof_mode_opt_name;
+    Attributes.program_mode_option_name;
+    Proof_using.proof_using_opt_name;
+  ]
+
+let classify_vernac e =
+  let static_classifier ~atts e = match e with
+    (* Univ poly compatibility: we run it now, so that we can just
+     * look at Flags in stm.ml.  Would be nicer to have the stm
+     * look at the entire dag to detect this option. *)
+    | VernacSetOption (_, l,_)
+      when CList.exists (CList.equal String.equal l)
+        options_affecting_stm_scheduling ->
+       VtSideff ([], VtNow)
+    (* Qed *)
+    | VernacAbort _ -> VtQed VtDrop
+    | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom)
+    | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque))
+    | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque)
+    (* Query *)
+    | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
+    | VernacCheckMayEval _ -> VtQuery
+    (* ProofStep *)
+    | VernacProof _
+    | VernacFocus _ | VernacUnfocus
+    | VernacSubproof _
+    | VernacCheckGuard
+    | VernacUnfocused
+    | VernacSolveExistential _ ->
+        VtProofStep { proof_block_detection = None }
+    | VernacBullet _ ->
+        VtProofStep { proof_block_detection = Some "bullet" }
+    | VernacEndSubproof ->
+        VtProofStep { proof_block_detection = Some "curly" }
+    (* StartProof *)
+    | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) ->
+      VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i)
+
+    | VernacDefinition (_,({v=i},_),ProveBody _) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+      VtStartProof(guarantee, idents_of_name i)
+    | VernacStartTheoremProof (_,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+      let ids = List.map (fun (({v=i}, _), _) -> i) l in
+      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+      VtStartProof (guarantee,ids)
+    | VernacFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+       let guarantee =
+         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
+       in
+        let ids, open_proof =
+          List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} ->
+            id::l, b || body_def = None) ([],false) l in
+        if open_proof
+        then VtStartProof (guarantee,ids)
+        else VtSideff (ids, VtLater)
+    | VernacCoFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+       let guarantee =
+         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
+       in
+        let ids, open_proof =
+          List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } ->
+            id::l, b || body_def = None) ([],false) l in
+        if open_proof
+        then VtStartProof (guarantee,ids)
+        else VtSideff (ids, VtLater)
+    (* Sideff: apply to all open branches. usually run on master only *)
+    | VernacAssumption (_,_,l) ->
+        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in
+        VtSideff (ids, VtLater)
+    | VernacPrimitive ((id,_),_,_) ->
+        VtSideff ([id.CAst.v], VtLater)
+    | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
+    | VernacInductive (_,l) ->
+        let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with
+        | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
+        | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
+           CList.map_filter (function
+            | AssumExpr({v=Names.Name n},_,_), _ -> Some n
+            | _ -> None) l) l in
+        VtSideff (List.flatten ids, VtLater)
+    | VernacScheme l ->
+        let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in
+        VtSideff (ids, VtLater)
+    | VernacCombinedScheme ({v=id},_) -> VtSideff ([id], VtLater)
+    | VernacBeginSection {v=id} -> VtSideff ([id], VtLater)
+    | VernacUniverse _ | VernacConstraint _
+    | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
+    | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
+    | VernacChdir _
+    | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
+    | VernacArguments _
+    | VernacReserve _
+    | VernacGeneralizable _
+    | VernacSetOpacity _ | VernacSetStrategy _
+    | VernacSetOption _
+    | VernacAddOption _ | VernacRemoveOption _
+    | VernacMemOption _ | VernacPrintOption _
+    | VernacGlobalCheck _
+    | VernacDeclareReduction _
+    | VernacExistingClass _ | VernacExistingInstance _
+    | VernacRegister _
+    | VernacNameSectionHypSet _
+    | VernacComments _
+    | VernacDeclareInstance _ -> VtSideff ([], VtLater)
+    (* Who knows *)
+    | VernacLoad _ -> VtSideff ([], VtNow)
+    (* (Local) Notations have to disappear *)
+    | VernacEndSegment _ -> VtSideff ([], VtNow)
+    (* Modules with parameters have to be executed: can import notations *)
+    | VernacDeclareModule (exp,{v=id},bl,_)
+    | VernacDefineModule (exp,{v=id},bl,_,_) ->
+        VtSideff ([id], if bl = [] && exp = None then VtLater else VtNow)
+    | VernacDeclareModuleType ({v=id},bl,_,_) ->
+        VtSideff ([id], if bl = [] then VtLater else VtNow)
+    (* These commands alter the parser *)
+    | VernacDeclareCustomEntry _
+    | VernacOpenCloseScope _ | VernacDeclareScope _
+    | VernacDelimiters _ | VernacBindScope _
+    | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
+    | VernacSyntaxExtension _
+    | VernacSyntacticDefinition _
+    | VernacRequire _ | VernacImport _ | VernacInclude _
+    | VernacDeclareMLModule _
+    | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow)
+    | VernacProofMode pm -> VtProofMode pm
+    | VernacInstance ((name,_),_,_,props,_) ->
+      let program, refine =
+        Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts)
+      in
+      if program || (props <> None && not refine) then
+        VtSideff (idents_of_name name.CAst.v, VtLater)
+      else
+        let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+        let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+        VtStartProof (guarantee, idents_of_name name.CAst.v)
+    (* Stm will install a new classifier to handle these *)
+    | VernacBack _ | VernacAbortAll
+    | VernacUndoTo _ | VernacUndo _
+    | VernacResetName _ | VernacResetInitial
+    | VernacRestart -> VtMeta
+    (* What are these? *)
+    | VernacRestoreState _
+    | VernacWriteState _ -> VtSideff ([], VtNow)
+    (* Plugins should classify their commands *)
+    | VernacExtend (s,l) ->
+        try Vernacextend.get_vernac_classifier s l
+        with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
+  in
+  let static_control_classifier ({ CAst.v ; _ } as cmd) =
+    (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+    (* XXX why is Fail not always Query? *)
+    if Vernacprop.has_Fail cmd then
+      (match static_classifier ~atts:v.attrs v.expr with
+         | VtQuery | VtProofStep _ | VtSideff _
+         | VtMeta as x -> x
+         | VtQed _ -> VtProofStep { proof_block_detection = None }
+         | VtStartProof _ | VtProofMode _ -> VtQuery)
+    else
+      static_classifier ~atts:v.attrs v.expr
+
+  in
+  static_control_classifier e
diff --git a/vernac/vernac_classifier.mli b/vernac/vernac_classifier.mli
new file mode 100644
index 0000000000..61bf3a503a
--- /dev/null
+++ b/vernac/vernac_classifier.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Vernacextend
+
+val string_of_vernac_classification : vernac_classification -> string
+
+(** What does a vernacular do *)
+val classify_vernac : Vernacexpr.vernac_control -> vernac_classification
+
+(**  *)
+val stm_allow_nested_proofs_option_name : string list
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4f3fc46c12..e8d84a67a3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -563,19 +563,19 @@ let program_inference_hook env sigma ev =
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")
 
-let vernac_set_used_variables ~pstate e : Declare.Proof.t =
+let vernac_set_used_variables ~pstate using : Declare.Proof.t =
   let env = Global.env () in
   let sigma, _ = Declare.Proof.get_current_context pstate in
   let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
-  let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
-  let l = Proof_using.process_expr env sigma e tys in
+  let terms = List.map snd (initial_goals (Declare.Proof.get pstate)) in
+  let using = Proof_using.definition_using env sigma ~using ~terms in
   let vars = Environ.named_context env in
-  List.iter (fun id ->
-    if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
-      user_err ~hdr:"vernac_set_used_variables"
-        (str "Unknown variable: " ++ Id.print id))
-    l;
-  let _, pstate = Declare.Proof.set_used_variables pstate l in
+  Names.Id.Set.iter (fun id ->
+      if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
+        user_err ~hdr:"vernac_set_used_variables"
+          (str "Unknown variable: " ++ Id.print id))
+    using;
+  let _, pstate = Declare.Proof.set_used_variables pstate ~using in
   pstate
 
 let vernac_set_used_variables_opt ?using pstate =
@@ -1215,9 +1215,11 @@ let msg_of_subsection ss id =
   in
   Pp.str kind ++ spc () ++ Id.print id
 
-let vernac_end_segment ~pm ({v=id} as lid) =
+let vernac_end_segment ~pm ~stack ({v=id} as lid) =
   let ss = Lib.find_opening_node id in
   let what_for = msg_of_subsection ss lid.v in
+  if Option.has_some stack then
+    CErrors.user_err (Pp.str "Command not supported (Open proofs remain)");
   Declare.Obls.check_solved_obligations ~pm ~what_for;
   match ss with
   | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
@@ -1401,31 +1403,9 @@ let warn_implicit_core_hint_db =
          (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. "
              ++ strbrk"Please specify a hint database.")
 
-let warn_deprecated_hint_without_locality =
-  CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated"
-    (fun () -> strbrk "The default value for hint locality is currently \
-    \"local\" in a section and \"global\" otherwise, but is scheduled to change \
-    in a future release. For the time being, adding hints outside of sections \
-    without specifying an explicit locality is therefore deprecated. It is \
-    recommended to use \"export\" whenever possible.")
-
-let check_hint_locality = function
-| OptGlobal ->
-  if Global.sections_are_opened () then
-  CErrors.user_err Pp.(str
-    "This command does not support the global attribute in sections.");
-| OptExport ->
-  if Global.sections_are_opened () then
-  CErrors.user_err Pp.(str
-    "This command does not support the export attribute in sections.");
-| OptDefault ->
-  if not @@ Global.sections_are_opened () then
-    warn_deprecated_hint_without_locality ()
-| OptLocal -> ()
-
 let vernac_remove_hints ~atts dbnames ids =
   let locality = Attributes.(parse option_locality atts) in
-  let () = check_hint_locality locality in
+  let () = Hints.check_hint_locality locality in
   let dbnames =
     if List.is_empty dbnames then
       (warn_implicit_core_hint_db (); ["core"])
@@ -1440,7 +1420,7 @@ let vernac_hints ~atts dbnames h =
     else dbnames
   in
   let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in
-  let () = check_hint_locality locality in
+  let () = Hints.check_hint_locality locality in
   Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x only_parsing =
@@ -1458,7 +1438,10 @@ let vernac_reserve bl =
     let env = Global.env() in
     let sigma = Evd.from_env env in
     let t,ctx = Constrintern.interp_type env sigma c in
-    let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t in
+    let t = Flags.without_option Detyping.print_universes (fun () ->
+        Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t)
+        ()
+    in
     let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl
@@ -1585,6 +1568,13 @@ let () =
 let () =
   declare_bool_option
     { optdepr  = false;
+      optkey   = ["Printing";"Raw";"Literals"];
+      optread  = (fun () -> !Constrextern.print_raw_literal);
+      optwrite = (fun b ->  Constrextern.print_raw_literal := b) }
+
+let () =
+  declare_bool_option
+    { optdepr  = false;
       optkey   = ["Printing";"All"];
       optread  = (fun () -> !Flags.raw_print);
       optwrite = (fun b -> Flags.raw_print := b) }
@@ -1662,6 +1652,13 @@ let () =
       optwrite = CWarnings.set_flags }
 
 let () =
+  declare_string_option
+    { optdepr  = false;
+      optkey   = ["Debug"];
+      optread  = CDebug.get_flags;
+      optwrite = CDebug.set_flags }
+
+let () =
   declare_bool_option
     { optdepr  = false;
       optkey   = ["Guard"; "Checking"];
@@ -1727,9 +1724,9 @@ let vernac_set_append_option ~locality key s =
 
 let vernac_set_option ~locality table v = match v with
 | OptionSetString s ->
-  (* We make a special case for warnings because appending is their
-  natural semantics *)
-  if CString.List.equal table ["Warnings"] then
+  (* We make a special case for warnings and debug flags because appending is
+  their natural semantics *)
+  if CString.List.equal table ["Warnings"] || CString.List.equal table ["Debug"] then
     vernac_set_append_option ~locality table s
   else
     let (last, prefix) = List.sep_last table in
@@ -2084,7 +2081,7 @@ let vernac_check_guard ~pstate =
 
 (* We interpret vernacular commands to a DSL that specifies their
    allowed actions on proof states *)
-let translate_vernac ~atts v = let open Vernacextend in match v with
+let translate_vernac ?loc ~atts v = let open Vernacextend in match v with
   | VernacAbortAll
   | VernacRestart
   | VernacUndo _
@@ -2195,9 +2192,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
     VtNoProof(fun () ->
         vernac_begin_section ~poly:(only_polymorphism atts) lid)
   | VernacEndSegment lid ->
-    VtReadProgram(fun ~pm ->
+    VtReadProgram(fun ~stack ~pm ->
         unsupported_attributes atts;
-        vernac_end_segment ~pm lid)
+        vernac_end_segment ~pm ~stack lid)
   | VernacNameSectionHypSet (lid, set) ->
     VtDefault(fun () ->
         unsupported_attributes atts;
@@ -2409,4 +2406,4 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
 
   (* Extensions *)
   | VernacExtend (opn,args) ->
-    Vernacextend.type_vernac ~atts opn args
+    Vernacextend.type_vernac ?loc ~atts opn args
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index cf233248d7..b30bbc3ce7 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -10,7 +10,8 @@
 
 (** Vernac Translation into the Vernac DSL *)
 val translate_vernac
-  : atts:Attributes.vernac_flags
+  : ?loc:Loc.t
+  -> atts:Attributes.vernac_flags
   -> Vernacexpr.vernac_expr
   -> Vernacextend.typed_vernac
 
@@ -26,4 +27,3 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
 val command_focus : unit Proof.focus_kind
 
 val allow_sprop_opt_name : string list
-val cumul_sprop_opt_name : string list
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 2e360cf969..46acaf7264 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -75,7 +75,6 @@ type search_request =
 type searchable =
   | SearchPattern of constr_pattern_expr
   | SearchRewrite of constr_pattern_expr
-  | SearchHead of constr_pattern_expr
   | Search of (bool * search_request) list
 
 type locatable =
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index ed63332861..df82382041 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -59,12 +59,12 @@ type typed_vernac =
   | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
   | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
   | VtReadProof of (pstate:Declare.Proof.t -> unit)
-  | VtReadProgram of (pm:Declare.OblState.t -> unit)
+  | VtReadProgram of (stack:Vernacstate.LemmaStack.t option -> pm:Declare.OblState.t -> unit)
   | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t)
   | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
   | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
 
-type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
+type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> typed_vernac
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -94,7 +94,7 @@ let warn_deprecated_command =
 
 (* Interpretation of a vernac command *)
 
-let type_vernac opn converted_args ~atts =
+let type_vernac opn converted_args ?loc ~atts =
   let depr, callback = vinterp_map opn in
   let () = if depr then
       let rules = Egramml.get_extend_vernac_rule opn in
@@ -106,7 +106,7 @@ let type_vernac opn converted_args ~atts =
       warn_deprecated_command pr;
   in
   let hunk = callback converted_args in
-  hunk ~atts
+  hunk ?loc ~atts
 
 (** VERNAC EXTEND registering *)
 
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index e1e3b4cfe5..27f6930dec 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -77,12 +77,12 @@ type typed_vernac =
   | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
   | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
   | VtReadProof of (pstate:Declare.Proof.t -> unit)
-  | VtReadProgram of (pm:Declare.OblState.t -> unit)
+  | VtReadProgram of (stack:Vernacstate.LemmaStack.t option -> pm:Declare.OblState.t -> unit)
   | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t)
   | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
   | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)
 
-type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
+type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> typed_vernac
 
 type plugin_args = Genarg.raw_generic_argument list
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index e5971e1aaa..4098401bf0 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -48,7 +48,7 @@ let interp_typed_vernac c ~pm ~stack =
     vernac_require_open_lemma ~stack
       (Vernacstate.LemmaStack.with_top ~f:(fun pstate -> f ~pstate));
     stack, pm
-  | VtReadProgram f -> f ~pm; stack, pm
+  | VtReadProgram f -> f ~stack ~pm; stack, pm
   | VtModifyProgram f ->
     let pm = f ~pm in stack, pm
   | VtDeclareProgram f ->
@@ -82,7 +82,7 @@ let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b =
   match !default_timeout, timeout with
   | _, Some n
   | Some n, None ->
-    (match Control.timeout n f x with
+    (match Control.timeout (float_of_int n) f x with
     | None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout)
     | Some x -> x)
   | None, None ->
@@ -151,7 +151,7 @@ let interp_control_flag ~time_header (f : control_flag) ~st
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
-let rec interp_expr ~atts ~st c =
+let rec interp_expr ?loc ~atts ~st c =
   let stack = st.Vernacstate.lemmas in
   let program = st.Vernacstate.program in
   vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
@@ -174,7 +174,7 @@ let rec interp_expr ~atts ~st c =
     Attributes.unsupported_attributes atts;
     vernac_load ~verbosely fname
   | v ->
-    let fv = Vernacentries.translate_vernac ~atts v in
+    let fv = Vernacentries.translate_vernac ?loc ~atts v in
     interp_typed_vernac ~pm:program ~stack fv
 
 and vernac_load ~verbosely fname =
@@ -206,13 +206,13 @@ and vernac_load ~verbosely fname =
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
   stack, pm
 
-and interp_control ~st ({ CAst.v = cmd } as vernac) =
+and interp_control ~st ({ CAst.v = cmd; loc } as vernac) =
   let time_header = mk_time_header vernac in
   List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
     cmd.control
     (fun ~st ->
        let before_univs = Global.universes () in
-       let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in
+       let pstack, pm = interp_expr ?loc ~atts:cmd.attrs ~st cmd.expr in
        let after_univs = Global.universes () in
        if before_univs == after_univs then pstack, pm
        else