diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-06 17:36:14 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-06 17:36:14 +0000 |
| commit | a59b644de4234fb7fe3fce28284979091f257130 (patch) | |
| tree | d5d8ff609aa9e4e582a06ca865a94eee1edbf182 /contrib/funind/indfun.ml | |
| parent | 3e3fa18a066feae44c10fc6e072059f4e9914656 (diff) | |
Plus de combinateurs sont passés de Util à Option. Le module Options
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/indfun.ml')
| -rw-r--r-- | contrib/funind/indfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 3102f1b5d..612be05e3 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -354,14 +354,14 @@ let register_struct is_rec fixpoint_exprl = | [(fname,_,bl,ret_type,body),_] when not is_rec -> Command.declare_definition fname - (Decl_kinds.Global,Options.boxed_definitions (),Decl_kinds.Definition) + (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition) bl None body (Some ret_type) (fun _ _ -> ()) | _ -> - Command.build_recursive fixpoint_exprl (Options.boxed_definitions()) + Command.build_recursive fixpoint_exprl (Flags.boxed_definitions()) 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 |