diff options
| author | barras | 2001-09-17 14:25:43 +0000 |
|---|---|---|
| committer | barras | 2001-09-17 14:25:43 +0000 |
| commit | d52de91b333e0c4bc0c326288757e89c341eb28c (patch) | |
| tree | 307398b63e610d77c86a977a11247914146b647e | |
| parent | 9b0512158dafc3a9e9275dc335ac0e63e776ecc4 (diff) | |
unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec les
sous-termes de (plus O O) ).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1975 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/clenv.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 1f67a42d83..b519968a3f 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -723,11 +723,8 @@ let constrain_clenv_to_subterm clause (op,cl) = else error "Bound 1" with ex when catchable_exception ex -> (match kind_of_term cl with - | IsApp (f,args) -> (try - matchrec f - with ex when catchable_exception ex -> - iter_fail matchrec args) - (* let n = Array.length args in + | IsApp (f,args) -> + let n = Array.length args in assert (n>0); let c1 = mkApp (f,Array.sub args 0 (n-1)) in let c2 = args.(n-1) in @@ -735,7 +732,6 @@ let constrain_clenv_to_subterm clause (op,cl) = matchrec c1 with ex when catchable_exception ex -> matchrec c2) - *) | IsMutCase(_,_,c,lf) -> (* does not search in the predicate *) (try matchrec c |