réparation Quote

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

1 files changed, 6 insertions, 0 deletions

diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 998418331..e4297ce85 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -264,6 +264,12 @@ let compute_ivs gl f cs =
                 lci;
 	      
               if !c_lhs = None & !v_lhs = None then i_can't_do_that ();
+
+	      (* The Cases predicate is a lambda; we assume no dependency *)
+	      let p = match kind_of_term p with
+		| IsLambda (_,_,p) -> pop p
+		| _ -> p
+	      in
               
               { normal_lhs_rhs = List.rev !n_lhs_rhs;
                 variable_lhs = !v_lhs;