From 8da844bb669317abbf3b4cc8d46457d7a40378d6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 6 Sep 2006 18:03:05 +0000 Subject: 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 --- toplevel/command.ml | 22 +++++++++++----------- 1 file 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 = -- cgit v1.2.3