|
9421
by barras
added the .vo checker (with independent Makefile) |
1 |
(************************************************************************)
|
2 |
(* v * The Coq Proof Assistant / The Coq Development Team *)
|
|
3 |
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
|
|
4 |
(* \VV/ **************************************************************)
|
|
5 |
(* // * This file is distributed under the terms of the *)
|
|
6 |
(* * GNU Lesser General Public License Version 2.1 *)
|
|
7 |
(************************************************************************)
|
|
8 |
||
9 |
(*i $Id: subtyping.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
|
|
10 |
||
11 |
(*i*)
|
|
12 |
open Univ |
|
13 |
open Term |
|
14 |
open Declarations |
|
15 |
open Environ |
|
16 |
(*i*)
|
|
17 |
||
18 |
val check_subtypes : env -> module_type_body -> module_type_body -> unit |
|
19 |
val check_equal : env -> module_type_body -> module_type_body -> unit |
|
20 |
||
21 |