diff options
| author | barras | 2005-06-08 09:30:39 +0000 |
|---|---|---|
| committer | barras | 2005-06-08 09:30:39 +0000 |
| commit | f7bb1cf476d3f1ecf555a2ddf5dd39bdf3c6f777 (patch) | |
| tree | b946d8e278d3a727bebee45febf110e931e9c9cf | |
| parent | 26e30a388e6950776fdbdbfe7483d83942ddfced (diff) | |
evar declarees avec mauvais type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7125 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/cases.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b6326c29e7..0f079bcf95 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1610,7 +1610,8 @@ let prepare_predicate_from_tycon loc dep env isevars tomatchs c = (* let c = whd_betadeltaiota env (evars_of isevars) c in *) (* We turn all subterms possibly dependent into an evar with maximum ctxt*) if isEvar c or List.exists (eq_constr c) allargs then - mkExistential env ~src:(loc, Evd.CasesType) isevars + e_new_evar isevars env ~src:(loc, Evd.CasesType) + (Retyping.get_type_of env (Evd.evars_of !isevars) c) else map_constr_with_full_binders push_rel build_skeleton env c in names, build_skeleton env (lift n c) |