Commit abe884cb authored by Andrei Paskevich's avatar Andrei Paskevich

Compute: provide an empty .mli

parent 25a381d4
......@@ -88,7 +88,7 @@ let normalize_goal_transf_few env =
} in
normalize_goal_transf p env
let () =
let () =
Trans.register_env_transform_l "compute_in_goal" normalize_goal_transf_all
~desc:"Performs@ possible@ computations@ in@ goal, including@ by@ \
declared@ rewrite@ rules"
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
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