diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-23 22:04:18 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-23 22:04:18 +0000 |
| commit | 681694ff2c34a41c4ea52cdb5a05c6d7ea921dfa (patch) | |
| tree | c3b0311e380f1328a995e1fd650ebd851ed092ef | |
| parent | cd21a1067dcf4506a69f86c42a593c21dca5abd5 (diff) | |
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
| -rw-r--r-- | proofs/clenv.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 29d3a5400..55e0fa5d3 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 |