diff options
| author | herbelin | 2006-09-06 18:03:05 +0000 |
|---|---|---|
| committer | herbelin | 2006-09-06 18:03:05 +0000 |
| commit | 8da844bb669317abbf3b4cc8d46457d7a40378d6 (patch) | |
| tree | 7c4cd79a562c3e1763990f6d248aaf99b9c4e3b5 | |
| parent | cecd63900e35eeeee5e8f75edc5ea57d7ce3cb91 (diff) | |
Finalement, interdiction des points fixes non totalement mutuellement
récursifs parce ce que la condition de garde élimine les appels
récursifs sur des sous-termes qui, par construction des types
inductifs, ne peuvent ultimement retomber sur un objet du type initial
de l'argument de décroissance (p.ex. un appel récursif sur p:positive
provenant d'un filtrage sur un z:Z ne sera d'emblée pas considérer
sous-terme car la destruction d'un positive ne donnera jamais un Z --
cf exemple de addZ dans une version d'avant aujourd'hui de
Sophia-Antipolis/MATHS/GROUPS/Z/Zadd.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9126 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/command.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 24d292d49f..b1918b3fc1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -491,17 +491,17 @@ let check_mutuality env fixl = let po = partial_order preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with | (x,Inr xge)::(y,Inr yge)::_ -> - if_verbose msg_warning - (let reason = - if List.mem x yge then - string_of_id y^" depends on "^string_of_id x - ^" but not conversely" - else if List.mem y xge then - string_of_id x^" depends on "^string_of_id y - ^" but not conversely" - else string_of_id y^" and "^string_of_id x - ^" are not mutually dependent" in - str ("Not a fully mutually defined fixpoint\n (e.g.: "^reason^")")) + let reason = + if List.mem x yge then + string_of_id y^" depends on "^string_of_id x + ^" but not conversely" + else if List.mem y xge then + string_of_id x^" depends on "^string_of_id y + ^" but not conversely" + else string_of_id y^" and "^string_of_id x + ^" are not mutually dependent" in + error + ("Not a fully mutually defined fixpoint\n (e.g.: "^reason^")") | _ -> () type fixpoint_kind = |