Commit 023cb64e authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

minor indentation changes

parent 5b53de4b
......@@ -7,6 +7,14 @@ open Axiom_result
open Axiom
open Side
type 'a fk = unit -> 'a
type ('a,'b) sk = 'a -> 'b fk -> 'b
(* type action_handler = *)
(* string -> state -> (state,state) sk -> state fk -> state *)
(*************************)
(* Auxialliary functions *)
(*************************)
......@@ -139,8 +147,8 @@ let binding_aux state y =
raise (Term_badly_formed error_message))
(* Print the goal and the potential errors that occured when executing the last
user command. *)
(* new_screen state : Print the goal and the potential errors that occured
when executing the last user command. *)
let new_screen state =
Formula.print_formula state.c_proof.goal state.param;
......@@ -177,8 +185,6 @@ let new_screen state =
{ state' with l_error_ref = [] }
(*****************)
(* Proof tactics *)
(*****************)
......@@ -1117,13 +1123,6 @@ let auto_intro : type a. a axiom_type -> state -> state =
(* Action type and definition *)
(******************************)
type 'a fk = unit -> 'a
type ('a,'b) sk = 'a -> 'b fk -> 'b
type action_handler =
string -> state -> (state,state) sk -> state fk -> state
(* action_name : The name of the action
action_short_description : Short description
action_description : Long description for the help command
......
open Term
open Proof
(*********************)
(* Type declarations *)
(*********************)
(* - c_proof : The current goal.
- danglings : All the other danglings node in the proof tree.
- input_history : The user input history.
......
......@@ -42,7 +42,6 @@ val add_error_fun : (unit -> unit) -> state -> state
val err_reset : state -> state
(*********************)
(* Parsing Functions *)
(*********************)
......@@ -72,6 +71,7 @@ val parse_string_list : string -> string list
comments, and normalize the input by removing supernumerary whitespaces. *)
val parse_input : string -> string list
(*************************)
(* Shell Input Functions *)
(*************************)
......
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