1 files changed, 36 insertions, 35 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b44c7cccb..94eb45fd3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -29,7 +29,6 @@ open Decl_kinds
 open Constrexpr
 open Redexpr
 open Lemmas
-open Misctypes
 open Locality
 open Vernacinterp
 
@@ -266,7 +265,7 @@ let print_namespace ns =
   let matches mp = match match_modulepath ns mp with
   | Some [] -> true
   | _ -> false in
-  let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in
+  let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in
   let constants_in_namespace =
     Cmap_env.fold (fun c (body,_) acc ->
       let kn = Constant.user c in
@@ -449,7 +448,7 @@ let start_proof_and_print k l hook =
         let evi = Evarutil.nf_evar_info sigma evi in
         let env = Evd.evar_filtered_env evi in
         try
-          let concl = EConstr.of_constr evi.Evd.evar_concl in
+          let concl = evi.Evd.evar_concl in
           if not (Evarutil.is_ground_env sigma env &&
                   Evarutil.is_ground_term sigma concl)
           then raise Exit;
@@ -518,7 +517,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 = Pfedit.by (Tactics.exact_proof c) in
-  save_proof (Vernacexpr.(Proved(Opaque,None)));
+  save_proof (Vernacexpr.(Proved(Proof_global.Opaque,None)));
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -637,7 +636,7 @@ let vernac_scheme l =
 let vernac_combined_scheme lid l =
   if Dumpglob.dump () then
     (Dumpglob.dump_definition lid false "def";
-     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Misctypes.AN (make ?loc @@ Ident id))) l);
+     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l);
  Indschemes.do_combined_scheme lid l
 
 let vernac_universe ~atts l =
@@ -672,7 +671,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
      else (idl,ty)) binders_ast in
   let mp =
     Declaremods.declare_module Modintern.interp_module_ast
-      id binders_ast (Enforce mty_ast) []
+      id binders_ast (Declaremods.Enforce mty_ast) []
   in
   Dumpglob.dump_moddef ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
@@ -855,7 +854,7 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 let vernac_instance ~atts abst sup inst props pri =
   let global = not (make_section_locality atts.locality) in
-  Dumpglob.dump_constraint inst false "inst";
+  Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
   let program_mode = Flags.is_program_mode () in
   ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
 
@@ -909,7 +908,7 @@ let vernac_set_used_variables e =
     if List.is_empty to_clear then (p, ())
     else
       let tac = Tactics.clear to_clear in
-      fst (Pfedit.solve SelectAll None tac p), ()
+      fst (Pfedit.solve Goal_select.SelectAll None tac p), ()
   end
 
 (*****************************)
@@ -977,7 +976,7 @@ let vernac_remove_hints ~atts dbs ids =
 
 let vernac_hints ~atts lb h =
   let local = enforce_module_locality atts.locality in
-  Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h)
+  Hints.add_hints ~local lb (Hints.interp_hints atts.polymorphic h)
 
 let vernac_syntactic_definition ~atts lid x y =
   Dumpglob.dump_definition lid false "syndef";
@@ -1131,15 +1130,16 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
   let names = rename prev_names names in
   let renaming_specified = Option.has_some !example_renaming in
 
-  if !rename_flag_required && not rename_flag then
-    user_err ~hdr:"vernac_declare_arguments"
-      (strbrk "To rename arguments the \"rename\" flag must be specified."
-    ++ spc () ++
-       match !example_renaming with
-       | None -> mt ()
-       | Some (o,n) ->
-          str "Argument " ++ Name.print o ++
-            str " renamed to " ++ Name.print n ++ str ".");
+  if !rename_flag_required && not rename_flag then begin
+    let msg =
+      match !example_renaming with
+      | None ->
+        strbrk "To rename arguments the \"rename\" flag must be specified."
+      | Some (o,n) ->
+        strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++
+        strbrk " into " ++ Name.print n ++ str "."
+    in user_err ~hdr:"vernac_declare_arguments" msg
+  end;
 
   let duplicate_names =
     List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
@@ -1268,7 +1268,7 @@ let vernac_reserve bl =
 
 let vernac_generalizable ~atts =
   let local = make_non_locality atts.locality in
-  Implicit_quantifiers.declare_generalizable local
+  Implicit_quantifiers.declare_generalizable ~local
 
 let _ =
   declare_bool_option
@@ -1465,22 +1465,22 @@ let _ =
       optkey   = ["Printing";"Universes"];
       optread  = (fun () -> !Constrextern.print_universes);
       optwrite = (fun b -> Constrextern.print_universes:=b) }
-     
+
 let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "dumping bytecode after compilation";
       optkey   = ["Dump";"Bytecode"];
-      optread  = Flags.get_dump_bytecode;
-      optwrite = Flags.set_dump_bytecode }
+      optread  = (fun () -> !Cbytegen.dump_bytecode);
+      optwrite = (:=) Cbytegen.dump_bytecode }
 
 let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "dumping VM lambda code after compilation";
       optkey   = ["Dump";"Lambda"];
-      optread  = Flags.get_dump_lambda;
-      optwrite = Flags.set_dump_lambda }
+      optread  = (fun () -> !Clambda.dump_lambda);
+      optwrite = (:=) Clambda.dump_lambda }
 
 let _ =
   declare_bool_option
@@ -1611,7 +1611,7 @@ let get_current_context_of_args = function
 
 let query_command_selector ?loc = function
   | None -> None
-  | Some (SelectNth n) -> Some n
+  | Some (Goal_select.SelectNth n) -> Some n
   | _ -> user_err ?loc ~hdr:"query_command_selector"
       (str "Query commands only support the single numbered goal selector.")
 
@@ -1619,17 +1619,16 @@ let vernac_check_may_eval ~atts redexp glopt rc =
   let glopt = query_command_selector ?loc:atts.loc glopt in
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma', c = interp_open_constr env sigma rc in
-  let c = EConstr.Unsafe.to_constr c in
   let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
   Evarconv.check_problems_are_solved env sigma';
-  let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
+  let sigma' = Evd.minimize_universes sigma' in
   let uctx = Evd.universe_context_set sigma' in
   let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in
-  let c = nf c in
   let j =
-    if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then
-      Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c))
+    if Evarutil.has_undefined_evars sigma' c then
+      Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c)
     else
+      let c = EConstr.to_constr sigma' c in
       (* OK to call kernel which does not support evars *)
       Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
   in
@@ -1652,7 +1651,9 @@ let vernac_check_may_eval ~atts redexp glopt rc =
 
 let vernac_declare_reduction ~atts s r =
   let local = make_locality atts.locality in
-  declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r))
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r))
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
@@ -1742,7 +1743,7 @@ let vernac_print ~atts env sigma =
        else str"There may remain asynchronous universe constraints"
      in
      begin match dst with
-     | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining
+     | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining
      | Some s -> dump_universes_gen univ s
      end
   | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
@@ -1912,7 +1913,7 @@ let vernac_subproof gln =
   Proof_global.simple_with_current_proof (fun _ p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
-    | Some (SelectNth n) -> Proof.focus subproof_cond () n p
+    | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
     | _ -> user_err ~hdr:"bracket_selector"
              (str "Brackets only support the single numbered goal selector."))
 
@@ -1970,7 +1971,7 @@ let vernac_load interp fname =
     interp x in
   let parse_sentence = Flags.with_option Flags.we_are_parsing
     (fun po ->
-    match Pcoq.Gram.entry_parse Pcoq.main_entry po with
+    match Pcoq.Gram.entry_parse Pvernac.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
@@ -2244,7 +2245,7 @@ let with_fail st b f =
       | HasNotFailed ->
           user_err ~hdr:"Fail" (str "The command has not failed!")
       | HasFailed msg ->
-          if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info
+          if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end