diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 10:33:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 10:33:04 +0000 |
| commit | e4e440a958ce9c49a39f01a3aaeb7603f77cd0a2 (patch) | |
| tree | cb33e267d8255a5fe381dfcb982d95286e8b9ef0 /kernel | |
| parent | 8b0e0dca812f1365b674c3721b10a4aa561573ae (diff) | |
Bug dans la gestion du contexte en présence de Fix dans le calcul de garde
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@978 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/typeops.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index ce28a60a8..860153ef4 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -540,7 +540,10 @@ let rec check_subterm_rec_meta env sigma vectn k def = (array_for_all (check_rec_call env n lst) typarray) && (array_for_all - (check_rec_call env (n+nbfix) (map_lift_fst_n nbfix lst)) + (check_rec_call + (push_rec_types recdef env) + (n+nbfix) + (map_lift_fst_n nbfix lst)) bodies) else let theDecrArg = List.nth l decrArg in @@ -554,7 +557,10 @@ let rec check_subterm_rec_meta env sigma vectn k def = (array_for_all (check_rec_call env n lst) typarray) && (array_for_all - (check_rec_call env (n+nbfix) (map_lift_fst_n nbfix lst)) + (check_rec_call + (push_rec_types recdef env) + (n+nbfix) + (map_lift_fst_n nbfix lst)) bodies) else let theBody = bodies.(i) in |