diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-17 15:48:45 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-17 15:48:45 +0000 |
| commit | f7e00f4bc292795bcef6b66c294a60cd4f61ccb0 (patch) | |
| tree | e6e09387898683bf26c37373745f588196bfcff5 /contrib/extraction/mlutil.ml | |
| parent | 97a93cc747342931c37e205c60d8398bd45a2f28 (diff) | |
merci les warnings de 3.09 ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7574 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/mlutil.ml')
| -rw-r--r-- | contrib/extraction/mlutil.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 5c842f159..b909eead5 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -256,7 +256,7 @@ type abbrev_map = global_reference -> ml_type option let type_expand env t = let rec expand = function | Tmeta {contents = Some t} -> expand t - | Tglob (r,l) as t -> + | Tglob (r,l) -> (match env r with | Some mlt -> expand (type_subst_list l mlt) | None -> Tglob (r, List.map expand l)) @@ -378,7 +378,7 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,c,l) -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () (*S Operations concerning De Bruijn indices. *) |