diff options
| author | Pierre-Marie Pédrot | 2018-09-28 18:55:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-06 14:51:54 +0200 |
| commit | 45e14bdb854fe5da40c2ed1d9ca575ae8d435d36 (patch) | |
| tree | 7bc43cb8e9561e1355ad99ddd0f10004e1bdf7d4 /kernel/constr.mli | |
| parent | 2089207415565e8a28816f53b61d9292d04f4c59 (diff) | |
Use lists instead of arrays in evar instances.
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 16919b705a..00051d7551 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -83,7 +83,7 @@ val mkFloat : Float64.t -> constr val mkMeta : metavariable -> constr (** Constructs an existential variable *) -type existential = Evar.t * constr array +type existential = Evar.t * constr list val mkEvar : existential -> constr (** Construct a sort *) @@ -203,9 +203,9 @@ val mkCoFix : cofixpoint -> constr (** {6 Concrete type for making pattern-matching. } *) -(** [constr array] is an instance matching definitional [named_context] in +(** [constr list] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) -type 'constr pexistential = Evar.t * 'constr array +type 'constr pexistential = Evar.t * 'constr list type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) |