Commit 8e8e4595 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

removed transformation induction_int_lex

parent 404a9dd8
...@@ -467,12 +467,14 @@ let induction_int_lex th_int = function ...@@ -467,12 +467,14 @@ let induction_int_lex th_int = function
with Exit -> [t] end with Exit -> [t] end
| _ -> assert false | _ -> assert false
(*
let () = let () =
Trans.register_env_transform_l "induction_int_lex" Trans.register_env_transform_l "induction_int_lex"
(fun env -> (fun env ->
let th_int = Env.find_theory env ["int"] "Int" in let th_int = Env.find_theory env ["int"] "Int" in
Trans.store (induction_int_lex th_int)) Trans.store (induction_int_lex th_int))
~desc:"Generate@ induction@ hypotheses@ for@ goals@ over@ integers." ~desc:"Generate@ induction@ hypotheses@ for@ goals@ over@ integers."
*)
(* (*
Local Variables: Local Variables:
......
Markdown is supported
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