diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-25 16:28:13 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-25 16:28:13 +0000 |
| commit | 3227a799ff592ce7e474c84b96df00aa4ed38055 (patch) | |
| tree | 993560ef76dda00efacb3307e714f7a08b7e369c /interp/constrintern.ml | |
| parent | d152948a08f22f80724247c19b76e493eb5b7963 (diff) | |
Useless use of maps in constr internalizing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16607 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ec8794e46..2adeb27cc 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) |