diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 53 |
1 files changed, 26 insertions, 27 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index c9b5144299..dafd1cc5e4 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,7 +29,8 @@ module NamedDecl = Context.Named.Declaration (*i*) let set_typeclass_transparency c local b = - Hints.add_hints ~local [typeclasses_db] + let locality = if local then Goptions.OptLocal else Goptions.OptGlobal in + Hints.add_hints ~locality [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) let classes_transparent_state () = @@ -38,17 +39,13 @@ let classes_transparent_state () = with Not_found -> TransparentState.empty let () = - Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state -let add_instance_hint inst path local info poly = - let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) - | IsGlobal gr -> Hints.IsGlobRef gr - in +let add_instance_hint inst path ~locality info poly = Flags.silently (fun () -> - Hints.add_hints ~local [typeclasses_db] + Hints.add_hints ~locality [typeclasses_db] (Hints.HintsResolveEntry - [info, poly, false, Hints.PathHints path, inst'])) () + [info, poly, false, Hints.PathHints path, inst])) () let is_local_for_hint i = match i.is_global with @@ -58,14 +55,16 @@ let is_local_for_hint i = add_instance_hint; don't ask hints to take discharge into account itself *) -let add_instance check inst = +let add_instance_base inst = let poly = Global.is_polymorphic inst.is_impl in - let local = is_local_for_hint inst in - add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local + let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in + add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality inst.is_info poly; - List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path - local pri poly) - (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) + List.iter (fun (path, pri, c) -> + let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in + add_instance_hint h path + ~locality pri poly) + (build_subclasses ~check:(not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) let mk_instance cl info glob impl = @@ -105,7 +104,7 @@ let discharge_instance (_, inst) = let is_local i = (i.is_global == None) let rebuild_instance inst = - add_instance true inst; + add_instance_base inst; inst let classify_instance inst = @@ -125,7 +124,7 @@ let instance_input : instance -> obj = let add_instance i = Lib.add_anonymous_leaf (instance_input i); - add_instance true i + add_instance_base i let warning_not_a_class = let name = "not-a-class" in @@ -313,29 +312,29 @@ let instance_hook info global imps ?hook cst = declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant info global imps ?hook name decl poly sigma term termtype = +let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let sigma, entry = DeclareDef.prepare_definition - ~allow_evars:false ~poly sigma decl ~types:(Some termtype) ~body:term in + ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in Declare.definition_message name; DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); instance_hook info global imps ?hook (GlobRef.ConstRef kn) -let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name = +let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = let subst = List.fold_left2 (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') [] subst (snd k.cl_context) in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in + let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); - instance_hook pri global imps (GlobRef.ConstRef cst) + instance_hook pri global impargs (GlobRef.ConstRef cst) -let declare_instance_program env sigma ~global ~poly name pri imps univdecl term termtype = +let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false dref imps; @@ -346,10 +345,10 @@ let declare_instance_program env sigma ~global ~poly name pri imps univdecl term in let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in let hook = DeclareDef.Hook.make hook in - let ctx = Evd.evar_universe_context sigma in + let uctx = Evd.evar_universe_context sigma in let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in let _ : DeclareObl.progress = - Obligations.add_definition ~name ~term ~univdecl ~scope ~poly ~kind ~hook typ ctx obls + Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = @@ -513,7 +512,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass = - if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass) + if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass) else tclass in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in |