Cas motif universel

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

1 files changed, 17 insertions, 17 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 3ab1dbdd48..29d3a54005 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -727,7 +727,7 @@ let unify_to_subterm clause (op,cl) =
 		 matchrec c)
           | _ -> error "Match_subterm")) 
   in 
-  if isMeta op then error "Match_subterm";
+(*  if isMeta op then error "Match_subterm";*)
   try matchrec cl
   with ex when catchable_exception ex ->
     raise (RefinerError (NoOccurrenceFound op))
@@ -736,22 +736,22 @@ let unify_to_subterm clause (op,cl) =
    a meta : BUG ?? *)
 let unify_to_subterm_list allow_K clause oplist t = 
   List.fold_right 
-    (fun op (clause,l) -> 
-       if occur_meta op then
-         let (clause',cl) =
-           try 
-	     (* This is up to some delta ... *)
-	     unify_to_subterm clause (strip_outer_cast op,t)
-           with RefinerError (NoOccurrenceFound _) when allow_K -> (clause,op)
-         in 
-	 (clause',cl::l)
-       else
-	 if not allow_K & not (dependent op t) then
-	   (* This is not up to delta ... *)
-	   raise (RefinerError (NoOccurrenceFound op))
-	 else
-	 (* Optimisation *)
-	 (clause,op::l))
+    (fun op (clause,l) ->
+      if isMeta op then
+	(clause,op::l)
+      else if occur_meta op then
+        let (clause',cl) =
+          try 
+	    (* This is up to some delta ... *)
+	    unify_to_subterm clause (strip_outer_cast op,t)
+          with RefinerError (NoOccurrenceFound _) when allow_K -> (clause,op)
+        in 
+	(clause',cl::l)
+      else if not allow_K & not (dependent op t) then
+	(* This is not up to delta ... *)
+	raise (RefinerError (NoOccurrenceFound op))
+      else
+	(clause,op::l))
     oplist 
     (clause,[])