diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index f44ac367..33891ad9 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -103,8 +103,13 @@ let instance_hook k pri global imps ?hook cst = let declare_instance_constant k pri global imps ?hook id poly uctx term termtype = let kind = IsDefinition Instance in + let uctx = + let levels = Univ.LSet.union (Universes.universes_of_constr termtype) + (Universes.universes_of_constr term) in + Universes.restrict_universe_context uctx levels + in let entry = - Declare.definition_entry ~types:termtype ~poly ~univs:uctx term + Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in @@ -165,7 +170,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in let env' = push_rel_context ctx env in evars := Evarutil.nf_evar_map !evars; - evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars; + evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars; let subst = List.map (Evarutil.nf_evar !evars) subst in if abstract then begin @@ -208,7 +213,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro let get_id = function | Ident id' -> id' - | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") + | Qualid (loc,id') -> (loc, snd (repr_qualid id')) in let props, rest = List.fold_left @@ -232,7 +237,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, Misctypes.IntroAnonymous, None) :: props), rest + (CHole (Loc.ghost, None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None) :: props), rest else props, rest) ([], props) k.cl_props in @@ -277,7 +282,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in let term = Option.map nf term in if not (Evd.has_undefined evm) && not (Option.is_empty term) then - let ctx = Evd.universe_context evm in + let ctx = Evd.universe_context_set evm in declare_instance_constant k pri global imps ?hook id poly ctx (Option.get term) termtype else if !refine_instance || Option.is_empty term then begin |