diff options
| author | ppedrot | 2013-03-11 21:35:19 +0000 |
|---|---|---|
| committer | ppedrot | 2013-03-11 21:35:19 +0000 |
| commit | 7c281301637f783beaec858a5fee665e99a6813b (patch) | |
| tree | be517bc917ed6dba36024659335763850918e5d5 /plugins | |
| parent | 14d27313ae3bdec2a61ce04cee9129b6e6775252 (diff) | |
Allowing (Co)Fixpoint to be defined local and Let-style.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index fd4e23de7a..131b4c0e22 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -364,7 +364,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition) bl None body (Some ret_type) (fun _ _ -> ()) | _ -> - Command.do_fixpoint fixpoint_exprl + Command.do_fixpoint Global fixpoint_exprl let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation |