- Fixed bugs and compatibilities issues in

  match_conjunction/match_disjunction/array_for_all_i
- Finally activate fine-tuned unfolding of iff in tauto: it breaks at
  only one place in the user contribs (FSetAVL_dep.v).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11726 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 5 deletions

diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4
index 5fd763c362..aadeb1a37c 100644
--- a/contrib/jprover/jprover.ml4
+++ b/contrib/jprover/jprover.ml4
@@ -87,7 +87,9 @@ let dest_coq_and ct =
             end
       | None -> jp_error "dest_coq_and"
 
-let is_coq_or = HP.is_disjunction
+let is_coq_or ct =
+  HP.is_disjunction ~strict:true ct
+  && List.length (snd (TR.decompose_app ct)) = 2
 
 (* return two subterms *)
 let dest_coq_or ct =
@@ -170,7 +172,7 @@ let sAPP ct t =
 
 
 let is_coq_exists ct =
-  if not (HP.is_conjunction ct) then false
+  if not (HP.is_conjunction ~strict:true ct) then false
   else let (hdapp,args) = TR.decompose_app ct in
      match args with
       | _::la::[] ->
@@ -203,9 +205,8 @@ let dest_coq_exists ct =
 
 
 let is_coq_and ct =
-  if (HP.is_conjunction ct) && not (is_coq_exists ct)
-  && not (is_coq_true ct) then true
-  else false
+  (HP.is_conjunction ~strict:true ct)
+  && List.length (snd (TR.decompose_app ct)) = 2
 
 
 (* Parsing modules: *)