diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-11 14:36:07 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-11 14:36:07 +0000 |
| commit | 6fd0922df95052a7adf68c0fc131bf32365386fb (patch) | |
| tree | f5b7a31b3d5dd412c022aa9df31645c902a325ca /contrib/funind/indfun_common.ml | |
| parent | 41e4d9cb0757f8057c0815fa0679e888e57ab604 (diff) | |
Bug corrections in Function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9065 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/indfun_common.ml')
| -rw-r--r-- | contrib/funind/indfun_common.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 20263c188..a7f7dbf82 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -274,6 +274,7 @@ type function_info = rect_lemma : constant option; rec_lemma : constant option; prop_lemma : constant option; + is_general : bool; (* Has this function been defined using general recursive definition *) } @@ -333,6 +334,7 @@ let subst_Function (_,subst,finfos) = rect_lemma = rect_lemma' ; rec_lemma = rec_lemma'; prop_lemma = prop_lemma'; + is_general = finfos.is_general } let classify_Function (_,infos) = Libobject.Substitute infos @@ -368,6 +370,7 @@ let discharge_Function (_,finfos) = rect_lemma = rect_lemma'; rec_lemma = rec_lemma'; prop_lemma = prop_lemma' ; + is_general = finfos.is_general } open Term @@ -442,7 +445,7 @@ let update_Function finfo = Lib.add_anonymous_leaf (in_Function finfo) -let add_Function f = +let add_Function is_general f = let f_id = id_of_label (con_label f) in let equation_lemma = find_or_none (mk_equation_id f_id) and correctness_lemma = find_or_none (mk_correct_id f_id) @@ -462,7 +465,9 @@ let add_Function f = rect_lemma = rect_lemma; rec_lemma = rec_lemma; prop_lemma = prop_lemma; - graph_ind = graph_ind + graph_ind = graph_ind; + is_general = is_general + } in update_Function finfos |