diff options
| author | msozeau | 2009-06-28 12:18:08 +0000 |
|---|---|---|
| committer | msozeau | 2009-06-28 12:18:08 +0000 |
| commit | 46a6319c3b96550039a97e169d58825d151cb4d4 (patch) | |
| tree | 687a7ae329de8af41e08c56b48013e05252cdfec /pretyping | |
| parent | 9fbe91637e1b2521c5bdc4d561247b0ee9dfcee2 (diff) | |
Improve return predicate inference by making the return type dependent
on a matched variable when it is of dependent type, when its type allows
it (no constructor in the real arguments).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12213 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 23b7661829..436e8e3c39 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1600,19 +1600,22 @@ let prepare_predicate_from_arsign_tycon loc env tomatchs sign arsign c = | Rel n when dependent tm c && signlen = 1 (* The term to match is not of a dependent type itself *) -> ((n, len) :: subst, len - signlen) - | Rel _ when not (dependent tm c) - && signlen > 1 (* The term is of a dependent type but does not appear in - the tycon, maybe some variable in its type does. *) -> + | Rel n when signlen > 1 (* The term is of a dependent type, + maybe some variable in its type appears in the tycon. *) -> (match tmtype with NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *) | IsInd (_, IndType(indf,realargs),_) -> - List.fold_left - (fun (subst, len) arg -> - match kind_of_term arg with + let subst = + if dependent tm c && List.for_all isRel realargs + then (n, 1) :: subst else subst + in + List.fold_left + (fun (subst, len) arg -> + match kind_of_term arg with | Rel n when dependent arg c -> ((n, len) :: subst, pred len) | _ -> (subst, pred len)) - (subst, len) realargs) + (subst, len) realargs) | _ -> (subst, len - signlen)) ([], nar) tomatchs arsign in |