diff options
| author | herbelin | 2002-01-24 13:43:25 +0000 |
|---|---|---|
| committer | herbelin | 2002-01-24 13:43:25 +0000 |
| commit | 92c7046e5349e3d98863af148ca451b81f819e3c (patch) | |
| tree | 027ac3e1283e32af3e6e810ab1563b55b4c1bdc5 | |
| parent | bef4e9e5842527ffc76c0ae9635a2188fd09602a (diff) | |
Réparation bug 'known_dependent'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2426 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b31854c93f..4d8c03d3e0 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1071,10 +1071,12 @@ let abstract_predicate env sigma indf = function let sign = make_arity_signature env true indf in (true, it_mkLambda_or_LetIn_name env pred sign) -let known_dependent = function +let rec known_dependent = function | None -> false | Some (PrLetIn ((_,copt),_)) -> copt <> None - | Some (PrProd _ | PrCcl _ | PrNotInd _) -> + | Some (PrNotInd (_,p)) -> known_dependent (Some p) + | Some (PrCcl _) -> false + | Some (PrProd _) -> anomaly "known_dependent: can only be used when patterns remain" (*****************************************************************************) |