diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 69 |
1 files changed, 34 insertions, 35 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 16b9e07fb2..3d38713e09 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,12 +39,11 @@ 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 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])) () @@ -55,16 +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 (Hints.IsGlobRef 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) -> let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in add_instance_hint h path - local pri poly) - (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) + ~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 = @@ -104,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 = @@ -124,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 @@ -304,54 +304,52 @@ let id_of_class cl = mip.(0).Declarations.mind_typename | _ -> assert false -let instance_hook info global imps ?hook cst = - Impargs.maybe_declare_manual_implicits false cst imps; +let instance_hook info global ?hook cst = let info = intern_info info in let env = Global.env () in let sigma = Evd.from_env env in 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 impargs ?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 - 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 scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs + ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in + instance_hook info global ?hook kn + +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 ~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) + let cst = (GlobRef.ConstRef cst) in + Impargs.maybe_declare_manual_implicits false cst impargs; + instance_hook pri global 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 impargs 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; let pri = intern_info pri in let env = Global.env () in let sigma = Evd.from_env env in declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst) in - let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in + let obls, _, term, typ = RetrieveObl.retrieve_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 ~impargs ~uctx typ obls in () -let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = +let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code @@ -359,12 +357,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let kind = Decls.(IsDefinition Instance) in - let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in + let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in let info = Lemmas.Info.make ~hook ~kind () in (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma termtype in + let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in (* spiwack: I don't know what to do with the status here. *) let lemma = match term with @@ -516,7 +514,8 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass = else tclass in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in - let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in + let flags = Pretyping.{ all_no_fail_flags with program_mode } in + let sigma, (c', imps') = interp_type_evars_impls ~flags ~impls env' sigma tclass in let imps = imps @ imps' in let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in |