blob: a0ac9677311e1ed83c08e44a26ff152a10845533 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
open Proofview
let constants = ref ([] : EConstr.t list)
let collect_constants () =
if (!constants = []) then
let open Coqlib in
let open EConstr in
let open Universes in
let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "hide" in
let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "hide_marker" in
constants := List.map (fun x -> of_constr (constr_of_global x))
[gr_H; gr_M];
!constants
else
!constants
let c_H () =
match collect_constants () with
it :: _ -> it
| _ -> failwith "could not obtain an internal representation of hide"
let c_M () =
match collect_constants () with
_ :: it :: _ -> it
| _ -> failwith "could not obtain an internal representation of hide_marker"
let package i = Goal.enter begin fun gl ->
Tactics.apply_in true false i
[None, (CAst.make (c_M (), Misctypes.NoBindings))] None
end
(*
let package i = Goal.enter begin fun gl ->
let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
let env = Goal.env gl in
let store = Goal.extra gl in
let concl = Tacmach.New.pf_concl in
let ty_i = ... in
let ev = Evarutil.new_evar in
mkApp (mkLambda(h_hyps_id, mkApp(c_h, [|ty_i|] , ev),
[| mkApp (c_hm, [| ty_ev; EConstr.mkVar i |]) |])
end
*)
let repackage _ = failwith "todo"
let hide_tactic i =
let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
Proofview.Goal.enter begin fun gl ->
let hyps = Environ.named_context_val (Proofview.Goal.env gl) in
if not (Termops.mem_named_context_val i hyps) then
(CErrors.user_err
(Pp.str ("no hypothesis named" ^ (Names.Id.to_string i))))
else
if Termops.mem_named_context_val h_hyps_id hyps then
tclTHEN (Tactics.revert [i; h_hyps_id]) (repackage ())
else
package i
end
|
