diff options
Diffstat (limited to 'pretyping/globEnv.ml')
| -rw-r--r-- | pretyping/globEnv.ml | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index 12788e5ec5..25510826cc 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -55,16 +55,16 @@ let env env = env.static_env let vars_of_env env = Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env) -let ltac_interp_name { ltac_idents ; ltac_genargs } = function - | Anonymous -> Anonymous - | Name id as na -> - try Name (Id.Map.find id ltac_idents) - with Not_found -> - if Id.Map.mem id ltac_genargs then - user_err (str "Ltac variable" ++ spc () ++ Id.print id ++ - spc () ++ str "is not bound to an identifier." ++ - spc () ++str "It cannot be used in a binder.") - else na +let ltac_interp_id { ltac_idents ; ltac_genargs } id = + try Id.Map.find id ltac_idents + with Not_found -> + if Id.Map.mem id ltac_genargs then + user_err (str "Ltac variable" ++ spc () ++ Id.print id ++ + spc () ++ str "is not bound to an identifier." ++ + spc () ++str "It cannot be used in a binder.") + else id + +let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar) let push_rel sigma d env = let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in @@ -182,6 +182,8 @@ let interp_ltac_variable ?loc typing_fun env sigma id = end; raise Not_found +let interp_ltac_id env id = ltac_interp_id env.lvar id + module ConstrInterpObj = struct type ('r, 'g, 't) obj = |