blob: 8d61006672ac9bacaf1a296f1d1b67c4ee0361bd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Environ
open Entries
open Constrexpr
open Misctypes
(** Module internalization errors *)
type module_internalization_error =
| NotAModuleNorModtype of string
| IncorrectWithInModule
| IncorrectModuleApplication
exception ModuleInternalizationError of module_internalization_error
(** Module expressions and module types are interpreted relatively to
possible functor or functor signature arguments. When the input kind
is ModAny (i.e. module or module type), we tries to interprete this ast
as a module, and in case of failure, as a module type. The returned
kind is never ModAny, and it is equal to the input kind when this one
isn't ModAny. *)
val interp_module_ast :
env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t
|
