diff options
| author | herbelin | 2011-11-16 08:46:46 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-16 08:46:46 +0000 |
| commit | 93b759f35a9f6544c5da9643330beb54ce255619 (patch) | |
| tree | 6990924e40d883eff674d60a0270bcd3e74a39a9 | |
| parent | 73e164c4bbb495703222a026e0b405c5b0bbb547 (diff) | |
Old typing bug in pattern-matching compilation (apparently w/o
consequences up to now, but maybe because this type is often later on
thrown away).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14663 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3fb7009564..932138f304 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1233,7 +1233,7 @@ and match_current pb tomatch = Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; let inst = List.map mkRel deps in { uj_val = applist (case, inst); - uj_type = substl inst typ } + uj_type = prod_applist typ inst } and compile_branch current names deps pb arsign eqn cstr = let sign, pb = build_branch current deps names pb arsign eqn cstr in |