diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-02 16:34:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-02 16:55:16 +0200 |
| commit | 67500967edf584fcddc41c74aea09d48ee80a03c (patch) | |
| tree | a0c46b71ac7536317462836a1336f8d497ab553e /interp/constrintern.mli | |
| parent | 94b201b0a7b03978d96b8f8c9d631e4fa4bda4b0 (diff) | |
Better struture for Ltac internalization environments in Constrintern.
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 46697253b..b6cae349d 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -67,7 +67,16 @@ val compute_internalization_env : env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Lazy.t Id.Map.t +type ltac_sign = { + ltac_vars : Id.Set.t; + (** Variables of Ltac which may be bound to a term *) + ltac_bound : Id.Set.t; + (** Other variables of Ltac *) + ltac_subst : glob_constr Lazy.t Id.Map.t; + (** Substitution for untyped terms *) +} + +val empty_ltac_sign : ltac_sign type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) |