1 files changed, 27 insertions, 24 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 76d427add..8cf3895fb 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -41,7 +41,7 @@ let _ = Goptions.declare_bool_option {
 let typeclasses_db = "typeclass_instances"
 
 let set_typeclass_transparency c local b = 
-  Hints.add_hints local [typeclasses_db] 
+  Hints.add_hints ~local [typeclasses_db]
     (Hints.HintsTransparencyEntry ([c], b))
     
 let _ =
@@ -50,24 +50,25 @@ let _ =
      let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
        | IsGlobal gr -> Hints.IsGlobRef gr
      in
-     let info =
-       let open Vernacexpr in
-       { info with hint_pattern =
-		   Option.map
-                     (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
-		     info.hint_pattern } in
      Flags.silently (fun () ->
-	Hints.add_hints local [typeclasses_db]
+       Hints.add_hints ~local [typeclasses_db]
 	  (Hints.HintsResolveEntry
 	     [info, poly, false, Hints.PathHints path, inst'])) ());
   Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
   Hook.set Typeclasses.classes_transparent_state_hook
     (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
 
+let intern_info {hint_priority;hint_pattern} =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  let hint_pattern = Option.map (Constrintern.intern_constr_pattern env sigma) hint_pattern in
+  {hint_priority;hint_pattern}
+
 (** TODO: add subinstances *)
 let existing_instance glob g info =
   let c = global g in
   let info = Option.default Hints.empty_hint_info info in
+  let info = intern_info info in
   let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
   let _, r = Term.decompose_prod_assum instance in
     match class_of_constr Evd.empty (EConstr.of_constr r) with
@@ -76,8 +77,8 @@ let existing_instance glob g info =
                          ~hdr:"declare_instance"
                          (Pp.str "Constant does not build instances of a declared type class.")
 
-let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
-let mismatched_props env n m = mismatched_ctx_inst env Properties n m
+let mismatched_params env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Parameters n m
+let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Properties n m
 
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
@@ -108,6 +109,7 @@ open Pp
 
 let instance_hook k info global imps ?hook cst =
   Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
+  let info = intern_info info in
   Typeclasses.declare_instance (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
@@ -135,7 +137,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
   ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let ({CAst.loc;v=instid}, pl) = instid in
-  let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
+  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let tclass, ids =
     match bk with
     | Decl_kinds.Implicit ->
@@ -143,7 +145,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	  (fun avoid (clname, _) ->
 	    match clname with
             | Some cl ->
-		let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in
+                let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
@@ -196,8 +198,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	in
 	let (_, ty_constr) = instance_constructor (k,u) subst in
         let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-        let sigma,_ = Evarutil.nf_evars_and_universes sigma in
-        Pretyping.check_evars env Evd.empty sigma termtype;
+        let sigma = Evd.minimize_universes sigma in
+        Pretyping.check_evars env (Evd.from_env env) sigma termtype;
         let univs = Evd.check_univ_decl ~poly sigma decl in
         let termtype = to_constr sigma termtype in
         let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
@@ -253,7 +255,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest
+                       ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
@@ -289,11 +291,11 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
       let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in
       let sigma = Evarutil.nf_evar_map_undefined sigma in
       (* Beware of this step, it is required as to minimize universes. *)
-      let sigma, _nf = Evarutil.nf_evar_map_universes sigma in
+      let sigma = Evd.minimize_universes sigma in
       (* Check that the type is free of evars now. *)
-      Pretyping.check_evars env Evd.empty sigma termtype;
+      Pretyping.check_evars env (Evd.from_env env) sigma termtype;
       let termtype = to_constr sigma termtype in
-      let term = Option.map (to_constr sigma) term in
+      let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
         if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
 	  declare_instance_constant k pri global imps ?hook id decl
             poly sigma (Option.get term) termtype
@@ -302,7 +304,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
             if program_mode then
 	      let hook vis gr _ =
 		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+                  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+                  let pri = intern_info pri in
 		  Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
 	      in
 	      let obls, constr, typ =
@@ -365,8 +368,8 @@ let context poly l =
   let sigma = Evd.from_env env in
   let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in
   (* Note, we must use the normalized evar from now on! *)
-  let sigma,_ = Evarutil.nf_evars_and_universes sigma in
-  let ce t = Pretyping.check_evars env Evd.empty sigma t in
+  let sigma = Evd.minimize_universes sigma in
+  let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
   let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
   let ctx =
     try named_of_rel_context fullctx
@@ -424,13 +427,13 @@ let context poly l =
       let decl = (Discharge, poly, Definitional) in
       let nstatus = match b with
       | None ->
-        pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
-          Vernacexpr.NoInline (CAst.make id))
+        pi3 (ComAssumption.declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
+               Declaremods.NoInline (CAst.make id))
       | Some b ->
         let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~univs ~types:t b in
         let hook = Lemmas.mk_hook (fun _ gr -> gr) in
-        let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in
+        let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
 	status && nstatus