diff options
| author | herbelin | 2009-11-08 14:50:15 +0000 |
|---|---|---|
| committer | herbelin | 2009-11-08 14:50:15 +0000 |
| commit | 0e3f27c1182c6a344a803e6c89779cfbca8f9855 (patch) | |
| tree | f9c5ec71af22e9cde44dd47875a72e3bfe24f8eb | |
| parent | 7baac26fccbd903f82f09e542aee1aa994d50c0d (diff) | |
Took local definitions into account in the test for deciding whether
the return clause of match is printed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12480 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/detyping.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 16520916cd..0d94838f0b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -162,9 +162,9 @@ let computable p k = sinon on perd la réciprocité de la synthèse (qui, lui, engendrera un prédicat non dépendant) *) - (nb_lam p = k+1) + let sign,ccl = decompose_lam_assum p in + (rel_context_length sign = k+1) && - let _,ccl = decompose_lam p in noccur_between 1 (k+1) ccl let avoid_flag isgoal = if isgoal then Some true else None @@ -683,6 +683,6 @@ let simple_cases_matrix_of_branches ind brns brs = (dummy_loc,ids,[p],c)) 0 brns brs -let return_type_of_predicate ind nparams n pred = - let nal,p = it_destRLambda_or_LetIn_names (n+1) pred in +let return_type_of_predicate ind nparams nrealargs_ctxt pred = + let nal,p = it_destRLambda_or_LetIn_names (nrealargs_ctxt+1) pred in (List.hd nal, Some (dummy_loc, ind, nparams, List.tl nal)), Some p |