diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 3 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 1 |
2 files changed, 0 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a88c5f79b7..b310dd6451 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -154,9 +154,6 @@ let valueOut = function | ast -> anomalylabstrm "valueOut" (str "Not a Dynamic ast: ") -(* To embed constr *) -let constrIn t = CDynamic (dummy_loc,constr_in t) - (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) let atomic_mactab = ref Idmap.empty let add_primitive_tactic s tac = diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 85fcb7e56a..6d7909b3ba 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -49,7 +49,6 @@ val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr) val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr val valueIn : value -> raw_tactic_arg -val constrIn : constr -> constr_expr (** Sets the debugger mode *) val set_debug : debug_info -> unit |