From 681694ff2c34a41c4ea52cdb5a05c6d7ea921dfa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 23 Dec 2002 22:04:18 +0000
Subject: Tentative d'interdire les K-abstractions si allow_K est faux et le
 motif n'a pas de métas (dans unify_to_subterm_list)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3479 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenv.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 29d3a54005..55e0fa5d37 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -727,22 +727,20 @@ let unify_to_subterm clause (op,cl) =
 		 matchrec c)
           | _ -> error "Match_subterm")) 
   in 
-(*  if isMeta op then error "Match_subterm";*)
   try matchrec cl
   with ex when catchable_exception ex ->
     raise (RefinerError (NoOccurrenceFound op))
 
-(* Possibly gives K-terms in case the operator does not contain 
-   a meta : BUG ?? *)
 let unify_to_subterm_list allow_K clause oplist t = 
   List.fold_right 
     (fun op (clause,l) ->
       if isMeta op then
-	(clause,op::l)
+	if allow_K then (clause,op::l)
+	else error "Match_subterm"
       else if occur_meta op then
         let (clause',cl) =
           try 
-	    (* This is up to some delta ... *)
+	    (* This is up to delta for subterms w/o metas ... *)
 	    unify_to_subterm clause (strip_outer_cast op,t)
           with RefinerError (NoOccurrenceFound _) when allow_K -> (clause,op)
         in 
-- 
cgit v1.2.3