diff options
| author | Pierre-Marie Pédrot | 2017-08-29 00:40:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-29 00:43:53 +0200 |
| commit | ece1cc059c26351d05a0ef41131c663c37cb7761 (patch) | |
| tree | 741aede5b10cc610dc3ea2c9881fb9c6b70f3e6a | |
| parent | 8ba24b7342c3885145406e588859a3e1e356987d (diff) | |
Binding an unsafe substitution function.
| -rw-r--r-- | src/tac2core.ml | 10 | ||||
| -rw-r--r-- | theories/Constr.v | 4 |
2 files changed, 14 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 4a4f9afd88..0fe4bc5fde 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -366,6 +366,15 @@ let prm_constr_kind : ml_tactic = function end | _ -> assert false +let prm_constr_substnl : ml_tactic = function +| [subst; k; c] -> + let subst = Value.to_list Value.to_constr subst in + let k = Value.to_int k in + let c = Value.to_constr c in + let ans = EConstr.Vars.substnl subst k c in + return (Value.of_constr ans) +| _ -> assert false + (** Patterns *) let prm_pattern_matches : ml_tactic = function @@ -653,6 +662,7 @@ let () = Tac2env.define_primitive (pname "string_set") prm_string_set let () = Tac2env.define_primitive (pname "constr_type") prm_constr_type let () = Tac2env.define_primitive (pname "constr_equal") prm_constr_equal let () = Tac2env.define_primitive (pname "constr_kind") prm_constr_kind +let () = Tac2env.define_primitive (pname "constr_substnl") prm_constr_substnl let () = Tac2env.define_primitive (pname "pattern_matches") prm_pattern_matches let () = Tac2env.define_primitive (pname "pattern_matches_subterm") prm_pattern_matches_subterm diff --git a/theories/Constr.v b/theories/Constr.v index d7cd3b58a3..bb02d94531 100644 --- a/theories/Constr.v +++ b/theories/Constr.v @@ -40,4 +40,8 @@ Ltac2 Type kind := [ Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind". +Ltac2 @ external substnl : constr list -> int -> constr -> constr := "ltac2" "constr_substnl". +(** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with + [r₁;...;rₙ] in [c]. *) + End Unsafe. |