diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-19 21:24:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-19 21:25:59 +0200 |
| commit | 8bd3e4eba54ace61f49a53b8ce74517de71006ec (patch) | |
| tree | 4ca4c75f1628e7500aae6d7d129eb9df72191f9d /engine/eConstr.ml | |
| parent | 234dc568769602cb91655929a344027a15f52845 (diff) | |
Exporting some functions of vars.ml as functions operating on EConstr.
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 46ac13b69..e5ac3792d 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -668,6 +668,9 @@ module Vars = struct exception LocalOccur let to_constr = unsafe_to_constr +let to_rel_decl = unsafe_to_rel_decl + +type substl = t list (** Operations that commute with evar-normalization *) let lift n c = of_constr (Vars.lift n (to_constr c)) @@ -677,6 +680,10 @@ let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (t let substl subst c = of_constr (Vars.substl (cast_list unsafe_eq subst) (to_constr c)) let subst1 c r = of_constr (Vars.subst1 (to_constr c) (to_constr r)) +let substnl_decl subst n d = of_rel_decl (Vars.substnl_decl (cast_list unsafe_eq subst) n (to_rel_decl d)) +let substl_decl subst d = of_rel_decl (Vars.substl_decl (cast_list unsafe_eq subst) (to_rel_decl d)) +let subst1_decl c d = of_rel_decl (Vars.subst1_decl (to_constr c) (to_rel_decl d)) + let replace_vars subst c = of_constr (Vars.replace_vars (cast_list_snd unsafe_eq subst) (to_constr c)) let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c)) |