aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-05 21:47:12 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-05 21:47:12 +0100
commitf8b624f7bec0406258eee4e08b0cec8d756da6ff (patch)
tree874c450f7d350455884d409bcfe6bafa44af7b47 /plugins
parenteb0feed6d22c11c44e7091c64ce5b1c9d5af987a (diff)
parent32baedf7a3aebb96f7dd2c7d90a1aef40ed93792 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--plugins/funind/indfun_common.mli2
3 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 7a933c04b..91a826c73 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -298,7 +298,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
(* let dur1 = System.time_difference tim1 tim2 in *)
(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
(* end; *)
- get_proof_clean true, Ephemeron.create hook
+ get_proof_clean true, CEphemeron.create hook
end
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index aa47e2619..2449678a1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -163,7 +163,7 @@ let save with_clean id const (locality,_,kind) hook =
(locality, ConstRef kn)
in
if with_clean then Pfedit.delete_current_proof ();
- Ephemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
+ CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
definition_message id
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 23f1da1ba..e5c756f56 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -47,7 +47,7 @@ val jmeq : unit -> Term.constr
val jmeq_refl : unit -> Term.constr
val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind ->
- unit Lemmas.declaration_hook Ephemeron.key -> unit
+ unit Lemmas.declaration_hook CEphemeron.key -> unit
(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
abort the proof