diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 10 |
1 files changed, 10 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 |