diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 17:16:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 603bfb392805fb8d1559d304bcf1b9c7b938bb6e (patch) | |
| tree | 37dde8996de9a02c03d518c69120b44827d4bc21 /API/API.mli | |
| parent | e3eb17a728d7b6874e67462e8a83fac436441872 (diff) | |
Getting rid of AUContext abstraction breakers in Recordops.
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index 9f7a6ded8..a661b34c5 100644 --- a/API/API.mli +++ b/API/API.mli @@ -84,6 +84,11 @@ sig val empty : t end + module AUContext : + sig + type t = Univ.AUContext.t + end + type universe_context = UContext.t [@@ocaml.deprecated "alias of API.Univ.UContext.t"] @@ -2884,7 +2889,7 @@ sig | Default_cs type obj_typ = Recordops.obj_typ = { o_DEF : Term.constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) o_TABS : Term.constr list; (** ordered *) o_TPARAMS : Term.constr list; (** ordered *) |