diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index f4b0015851..b0dba2485a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -146,7 +146,7 @@ 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 = @@ -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 |