diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-07 22:48:31 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-07 22:48:31 +0000 |
| commit | d44af32d0946b62fe2db9efa47fb8b7063d0024d (patch) | |
| tree | 3e6684c3976723ce117b28b96061fe95783790c7 | |
| parent | c80fbaac51c390d11e75763cd67b999eb8a671ff (diff) | |
Fix big de Bruijn bug in mutually recursive definitions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10763 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index a8bc546aa..c29d677f5 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -390,6 +390,7 @@ let interp_recursive fixkind l boxed = let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in + let recdefs = List.length rec_sign in (* List.iter (check_evars env_rec Evd.empty evd) fixdefs; *) (* List.iter (check_evars env Evd.empty evd) fixtypes; *) @@ -422,7 +423,8 @@ let interp_recursive fixkind l boxed = let possible_indexes = List.map2 compute_possible_guardness_evidences wfl fixtypes in let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), - Array.of_list fixtypes, Array.of_list (List.map (subst_vars fixnames) fixdefs) + Array.of_list fixtypes, + Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l |