diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 9 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 9 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
5 files changed, 18 insertions, 10 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 25a7675113..ca09cad1f3 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -353,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) in let names = ref [new_princ_name] in let hook = - fun new_principle_type _ _ -> + fun new_principle_type _ _ _ _ -> if Option.is_empty sorts then (* let id_of_f = Label.to_id (con_label f) in *) @@ -385,7 +385,8 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) - save false new_princ_name entry g_kind ~hook + let uctx = Evd.evar_universe_context sigma in + save false new_princ_name entry ~hook uctx g_kind with e when CErrors.noncritical e -> begin begin @@ -539,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ this_block_funs 0 (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) - (fun _ _ _ -> ()) + (fun _ _ _ _ _ -> ()) with e when CErrors.noncritical e -> begin begin @@ -614,7 +615,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ this_block_funs !i (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) - (fun _ _ _ -> ()) + (fun _ _ _ _ _ -> ()) in const with Found_type i -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f9938c0356..cba3cc3d42 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -129,7 +129,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const ?hook (locality,_,kind) = +let save with_clean id const ?hook uctx (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> @@ -144,7 +144,7 @@ let save with_clean id const ?hook (locality,_,kind) = (locality, ConstRef kn) in if with_clean then Proof_global.discard_current (); - Lemmas.call_hook ?hook ~fix_exn l r; + Lemmas.call_hook ?hook ~fix_exn uctx [] l r; definition_message id let with_full_print f a = diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 9584649cff..1e0b95df34 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -42,7 +42,14 @@ val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr -val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit +val save + : bool + -> Id.t + -> Safe_typing.private_constants Entries.definition_entry + -> ?hook:Lemmas.declaration_hook + -> UState.t + -> Decl_kinds.goal_kind + -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a8517e9ab1..8746c37309 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1310,7 +1310,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); - let hook _ _ = + let hook _ _ _ _ = let opacity = let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in @@ -1560,7 +1560,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook _ _ = + let hook _ _ _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 7da4464e59..2d833a2cde 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1989,7 +1989,7 @@ let add_morphism_infer atts m n = Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in - let hook _ = function + let hook _ _ _ = function | Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info |