Commit 13c872fa authored by François Bobot's avatar François Bobot
Browse files

Session rewrite fix :

 - goal name are correctly printed when no explanation are provided
 - explanation becomes an abstract type
parent 804401a4
...@@ -539,7 +539,7 @@ let init = ...@@ -539,7 +539,7 @@ let init =
| S.Transf _ -> !image_transf); | S.Transf _ -> !image_transf);
goals_model#set ~row:row#iter ~column:name_column goals_model#set ~row:row#iter ~column:name_column
(match any with (match any with
| S.Goal g -> default_option "" g.S.goal_expl | S.Goal g -> S.goal_expl g
| S.Theory th -> th.S.theory_name.Ident.id_string | S.Theory th -> th.S.theory_name.Ident.id_string
| S.File f -> Filename.basename f.S.file_name | S.File f -> Filename.basename f.S.file_name
| S.Proof_attempt a -> | S.Proof_attempt a ->
......
...@@ -62,7 +62,7 @@ type proof_attempt_status = ...@@ -62,7 +62,7 @@ type proof_attempt_status =
| Done of Call_provers.prover_result (** external proof done *) | Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *) | InternalFailure of exn (** external proof aborted by internal error *)
type expl = string option type expl
(** An explanation gives hint about how the goal has been produced. (** An explanation gives hint about how the goal has been produced.
Allow to reattach proof_attempt to goal when the source file has been Allow to reattach proof_attempt to goal when the source file has been
modified. modified.
...@@ -296,7 +296,7 @@ val set_timelimit : int -> 'key proof_attempt -> unit ...@@ -296,7 +296,7 @@ val set_timelimit : int -> 'key proof_attempt -> unit
val add_transformation : val add_transformation :
keygen:'key keygen -> keygen:'key keygen ->
goal:('goal -> Ident.ident * string option * Task.task) -> goal:('goal -> Ident.ident * expl * Task.task) ->
string -> string ->
'key goal -> 'key goal ->
'goal list -> 'goal list ->
...@@ -378,7 +378,7 @@ module AddTransf (X : sig ...@@ -378,7 +378,7 @@ module AddTransf (X : sig
val keygen : key keygen val keygen : key keygen
type goal type goal
val goal : goal -> Ident.ident * string option * Task.task val goal : goal -> Ident.ident * expl * Task.task
type transf type transf
val fold_transf : ('a -> goal -> 'a) -> 'a -> Task.task -> transf -> 'a val fold_transf : ('a -> goal -> 'a) -> 'a -> Task.task -> transf -> 'a
...@@ -391,7 +391,7 @@ module AddFile(X : sig ...@@ -391,7 +391,7 @@ module AddFile(X : sig
val keygen : key keygen val keygen : key keygen
type goal type goal
val goal : goal -> Ident.ident * string option * Task.task val goal : goal -> Ident.ident * expl * Task.task
type theory type theory
val fold_theory : ('a -> goal -> 'a) -> 'a -> theory -> 'a val fold_theory : ('a -> goal -> 'a) -> 'a -> theory -> 'a
......
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