diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-07 16:09:23 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-07 16:09:23 +0000 |
| commit | aaf608630f8ae0ed9cfb4731bff0bd114cafc430 (patch) | |
| tree | 97f38088afcdcee4492e91c7e64aa258bddeb923 | |
| parent | 52d0524137d3bdd2c8afad483f8d731f4e19a28a (diff) | |
Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn bug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14168 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index cd4400f18..87b372c38 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -1531,7 +1531,7 @@ let constr_of_pat env isevars arsign pat avoid = | PatCstr (l,((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in let IndType (indf, _) = - try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) + try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env {uj_val = ty; uj_type = Typing.type_of env !isevars ty} in @@ -1545,7 +1545,7 @@ let constr_of_pat env isevars arsign pat avoid = List.fold_right2 (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) -> let pat', sign', arg', typ', argtypargs, n', avoid = - typ env (lift (n - m) t, []) ua avoid + typ env (substl args (liftn (List.length sign) (succ (List.length args)) t), []) ua avoid in let args' = arg' :: List.map (lift n') args in let env' = push_rels sign' env in |