diff options
| author | Pierre-Marie Pédrot | 2017-07-27 16:29:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-27 16:38:44 +0200 |
| commit | fee254e2f7a343629df31d5a39780ca4698de571 (patch) | |
| tree | 2a1349689abdb2ba76515ad32142e13e17e55d1c /src/tac2expr.mli | |
| parent | bc9a18bd48fb43a2aedd9c11df7a3e4244074120 (diff) | |
Cleaning up code in internalization.
Diffstat (limited to 'src/tac2expr.mli')
| -rw-r--r-- | src/tac2expr.mli | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli index b268e70cb3..e564dbde78 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -53,9 +53,18 @@ type 'a glb_typexpr = | GTypTuple of 'a glb_typexpr list | GTypRef of type_constant * 'a glb_typexpr list +type glb_alg_type = { + galg_constructors : (uid * int glb_typexpr list) list; + (** Constructors of the algebraic type *) + galg_nconst : int; + (** Number of constant constructors *) + galg_nnonconst : int; + (** Number of non-constant constructors *) +} + type glb_typedef = | GTydDef of int glb_typexpr option -| GTydAlg of (uid * int glb_typexpr list) list +| GTydAlg of glb_alg_type | GTydRec of (lid * mutable_flag * int glb_typexpr) list | GTydOpn |