diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-22 15:31:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-23 12:09:14 +0200 |
| commit | 74ddca99c649f2f8c203582a9b82bddf64fb6b52 (patch) | |
| tree | f23aa6340c2630619864666ef5eed257d3d765d9 /tactics/tactics.mli | |
| parent | d23c7539887366202bc370d0f80c26a557486e1c (diff) | |
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0e92e7eb9..5b7ad1f88 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -64,7 +64,6 @@ val intro_using : Id.t -> unit Proofview.tactic val intro_mustbe_force : Id.t -> unit Proofview.tactic val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intros_using : Id.t list -> unit Proofview.tactic -val intro_erasing : Id.t -> tactic val intros_replacing : Id.t list -> unit Proofview.tactic val intros : unit Proofview.tactic @@ -256,8 +255,6 @@ val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) -> val general_elim : evars_flag -> constr with_bindings -> eliminator -> tactic -val general_elim_in : evars_flag -> Id.t -> - constr with_bindings -> eliminator -> tactic val default_elim : evars_flag -> constr with_bindings -> unit Proofview.tactic val simplest_elim : constr -> unit Proofview.tactic @@ -328,7 +325,6 @@ val setoid_symmetry : unit Proofview.tactic Hook.t val symmetry_red : bool -> unit Proofview.tactic val symmetry : unit Proofview.tactic val setoid_symmetry_in : (Id.t -> unit Proofview.tactic) Hook.t -val symmetry_in : Id.t -> unit Proofview.tactic val intros_symmetry : clause -> unit Proofview.tactic val setoid_transitivity : (constr option -> unit Proofview.tactic) Hook.t |