diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 29 |
1 files changed, 14 insertions, 15 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 52c1e1cf98..b0dba2485a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -69,7 +69,7 @@ let existing_instance glob g info = let c = Nametab.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 instance, _ = Typeops.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 | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c) @@ -146,10 +146,10 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook k pri global imps ?hook (ConstRef cst); id -let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype = +let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype = let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if program_mode then - let hook _ vis gr = + let hook _ _ vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; let pri = intern_info pri in @@ -189,10 +189,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id in ignore (Pfedit.by init_refine) else if Flags.is_auto_intros () then - ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); + ignore (Pfedit.by (Tactics.auto_intros_tac ids)); (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) () -let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props len = +let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -275,7 +275,7 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro 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 else if program_mode || refine || Option.is_empty term then - declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype + declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining."); id @@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id else do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode - cty k u ctx ctx' pri decl imps subst id props len + cty k u ctx ctx' pri decl imps subst id props let named_of_rel_context l = let open Vars in @@ -370,25 +370,24 @@ let context poly l = user_err Pp.(str "Anonymous variables not allowed in contexts.") in let univs = - let uctx = Evd.universe_context_set sigma in match ctx with | [] -> assert false - | [_] -> - if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) - else Monomorphic_const_entry uctx + | [_] -> Evd.const_univ_entry ~poly sigma | _::_::_ -> + (** TODO: explain this little belly dance *) if Lib.sections_are_opened () then begin + let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; - if poly then Polymorphic_const_entry Univ.UContext.empty + if poly then Polymorphic_const_entry ([||], Univ.UContext.empty) else Monomorphic_const_entry Univ.ContextSet.empty end - else if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) + else if poly then + Evd.const_univ_entry ~poly sigma else begin + let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; Monomorphic_const_entry Univ.ContextSet.empty end |