diff options
| author | herbelin | 2005-11-08 17:14:52 +0000 |
|---|---|---|
| committer | herbelin | 2005-11-08 17:14:52 +0000 |
| commit | 4a7555cd875b0921368737deed4a271450277a04 (patch) | |
| tree | ea296e097117b2af5606e7365111f5694d40ad9a /kernel/inductive.ml | |
| parent | 8d94b3c7f4c51c5f78e6438b7b3e39f375ce9979 (diff) | |
Nettoyage suite à la détection par défaut des variables inutilisées par ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index bf64dfda08..235c82b1a8 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -593,7 +593,6 @@ let check_one_fix renv recpos def = | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> List.for_all (check_rec_call renv) l && array_for_all (check_rec_call renv) typarray && - let nbfix = Array.length typarray in let decrArg = recindxs.(i) in let renv' = push_fix_renv renv recdef in if (List.length l < (decrArg+1)) then @@ -613,7 +612,7 @@ let check_one_fix renv recpos def = bodies in array_for_all (fun b -> b) ok_vect - | Const kn as c -> + | Const kn -> (try List.for_all (check_rec_call renv) l with (FixGuardError _ ) as e -> if evaluable_constant kn renv.env then @@ -705,7 +704,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = +let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = let (minds, rdef) = inductive_of_mutfix env fix in for i = 0 to Array.length bodies - 1 do let (fenv,body) = rdef.(i) in |