diff options
| author | glondu | 2011-10-28 08:35:06 +0000 |
|---|---|---|
| committer | glondu | 2011-10-28 08:35:06 +0000 |
| commit | 97da8221e0097ed365f0a99e4960148424a59734 (patch) | |
| tree | 7a0d1b1bc8995dd456b38863674a65230ace957f /tactics | |
| parent | 7a10a8a17928df1da29b4f69a2b54ac83a3e1fc3 (diff) | |
Remove dynamic stuff from constr_expr and glob_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |