Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 17f2d252 authored by Sylvain Dailler's avatar Sylvain Dailler

removed dead code, irrelevant comments.

parent 0fc3a92d
(* TODO: all occurences of Format.eprintf in this file should be
replaced by proper server notifications *)
let has_extension f =
try
let _ = Filename.chop_extension f in true
......
......@@ -89,20 +89,6 @@ type session = {
session_prover_ids : int Hprover.t;
}
let dummy_session =
{
proofAttempt_table = Hint.create 23;
next_proofAttemptID = 0;
proofNode_table = Hint.create 23;
next_proofNodeID = 0;
trans_table = Hint.create 23;
next_transID = 0;
session_dir = "";
session_files = Hstr.create 23;
session_shape_version = 0;
session_prover_ids = Hprover.create 23;
}
let theory_parent s th =
Hstr.find s.session_files th.theory_parent_name
......
......@@ -16,8 +16,6 @@ unique identifiers of type [proofNodeId]
type session
val dummy_session: session
type proofNodeID
val print_proofNodeID : Format.formatter -> proofNodeID -> unit
type transID
......
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