diff options
| author | Pierre-Marie Pédrot | 2014-06-08 20:39:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-08 20:53:51 +0200 |
| commit | 0dfaecc2de2306ff9674a4aa3e546d3123015169 (patch) | |
| tree | d031ad991f690c7fa1f77213dcc8af0a9df27a0c /plugins/funind/recdef.ml | |
| parent | 2fceefe036f5f8289fd4667ade8b3240a11579d7 (diff) | |
Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
the checker, and it was not used before that anyway.
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 08d8ca3914..d8f006f518 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1320,7 +1320,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) (gls_type, ctx) - (Future.mk_hook hook); + (Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () then ignore (by (Proofview.V82.tactic (tclIDTAC))) @@ -1417,7 +1417,7 @@ let (com_eqn : int -> Id.t -> (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) - (Future.mk_hook (fun _ _ -> ())); + (Lemmas.mk_hook (fun _ _ -> ())); ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> @@ -1537,5 +1537,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - ctx (Future.mk_hook hook)) + ctx (Lemmas.mk_hook hook)) () |