diff options
| author | Arnaud Spiwack | 2013-11-25 14:25:29 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-11-25 16:22:41 +0100 |
| commit | 51d4da4ac126b4b3bb033ec88253866345594e01 (patch) | |
| tree | 417a1144c28cf691cfa1819b01e7f71ad3ffbb19 /plugins/funind/indfun_common.ml | |
| parent | 494ef20fc93dbe7bf373f713284f08b034da9075 (diff) | |
Remove the Hiddentac module.
Since the new proof engine, Hiddentac has been essentially trivial.
Here is what happened to the functions defined there
- Aliases, or tactics that were trivial to inline were systematically inlined
- Tactics used only in tacinterp have been moved to tacinterp
- Other tactics have been moved to a new module Tactics.Simple.
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e5b975e149..b7072ea3bd 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -3,7 +3,6 @@ open Pp open Libnames open Globnames open Refiner -open Hiddentac let mk_prefix pre id = Id.of_string (pre^(Id.to_string id)) let mk_rel_id = mk_prefix "R_" let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct" @@ -484,7 +483,7 @@ let jmeq_refl () = with e when Errors.noncritical e -> raise (ToShow e) let h_intros l = - tclMAP (fun x -> Proofview.V82.of_tactic (h_intro x)) l + tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" |