diff options
author | 2013-08-08 18:52:52 +0000 | |
---|---|---|
committer | 2013-08-08 18:52:52 +0000 | |
commit | c81254903e1e50a2305cd48ccfb673d9737afc48 (patch) | |
tree | 622d6167cb84e4232794145801ab5ca87bde25fa /plugins/funind/recdef.ml | |
parent | 80aba8d52c650ef8e4ada694c20bf12c15849694 (diff) |
get rid of closures in global/proof state
In some cases, an 'a -> 'b field is changed into an ('a -> b') option
field so that one can forget the closures and marshal the resulting
state
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 85f007b7-540e-0410-9357-904b9bb8a0f7
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 68b291ff9..e6f682635 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1313,7 +1313,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) sign gls_type - hook ; + (Some hook) ; if Indfun_common.is_strict_tcc () then by (tclIDTAC) @@ -1406,7 +1406,7 @@ let (com_eqn : int -> Id.t -> let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in (start_proof eq_name (Global, Proof Lemma) - (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); + (Environ.named_context_val env) equation_lemma_type None; by (start_equation f_ref terminate_ref (fun x -> @@ -1523,6 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - hook) + (Some hook)) () |