Commit 921740fc authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Added clear_but tactic.

parent 4c1e7f8b
...@@ -603,6 +603,7 @@ let unfold unf h = ...@@ -603,6 +603,7 @@ let unfold unf h =
end end
| _ -> [d]) None | _ -> [d]) None
(* from task [delta, name1, name2, ... namen |- G] build the task [name1, name2, ... namen |- G] *)
let clear_but (l: prsymbol list) = let clear_but (l: prsymbol list) =
Trans.decl Trans.decl
(fun d -> (fun d ->
...@@ -656,10 +657,9 @@ let () = wrap_and_register ~desc:"remove a literal using an equality on it" ...@@ -656,10 +657,9 @@ let () = wrap_and_register ~desc:"remove a literal using an equality on it"
"subst" "subst"
(Tlsymbol Ttrans) subst (Tlsymbol Ttrans) subst
(* TODO give a list of hypothesis *)
let () = wrap_and_register ~desc:"clear all axioms but the hypothesis argument" let () = wrap_and_register ~desc:"clear all axioms but the hypothesis argument"
"clear_but" "clear_but"
(Tprsymbol Ttrans) (fun x -> clear_but [x]) (Tprlist Ttrans) clear_but
let () = wrap_and_register ~desc:"left transform a goal of the form A \\/ B into A" let () = wrap_and_register ~desc:"left transform a goal of the form A \\/ B into A"
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment