diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 6 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ec8794e468..2adeb27cc5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -632,7 +632,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = else if Id.equal id ldots_var then if ntnvars != [] then GVar (loc,id), [], [], [] else error_ldots_var loc - else if Id.Map.mem id unbndltacvars then + else if Id.Set.mem id unbndltacvars then (* Is [id] bound to a free name in ltac (this is an ltac error message) *) user_err_loc (loc,"intern_var", str "variable " ++ pr_id id ++ str " should be bound to a term.") @@ -1659,9 +1659,9 @@ let scope_of_type_kind = function | OfType typ -> compute_type_scope typ | WithoutTypeConstraint -> None -type ltac_sign = Id.t list * unbound_ltac_var_map +type ltac_sign = Id.t list * Id.Set.t -let empty_ltac_sign = ([], Id.Map.empty) +let empty_ltac_sign = ([], Id.Set.empty) let intern_gen kind sigma env ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 32e878165c..2a80856827 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -68,7 +68,7 @@ val compute_internalization_env : env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type ltac_sign = Id.t list * unbound_ltac_var_map +type ltac_sign = Id.t list * Id.Set.t type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) |