Interface of the argument to Continuationals.Make greately simplified. The

following functions have been removed:
 - id_tactic
 - get_status
 - get_proof
 - set_goals

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index c93aeb6547255185ae535f40d90b657feebd319c..f85c13bbb84a1d9be4c76aed4e06ba003e2a0e57 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -492,23 +492,11 @@ let eval_tactical ~disambiguate_tactic status tac =
  
    type tactic = input_status -> output_status
  
-   let id_tactic = apply_tactic ("",0,(GrafiteAst.IdTac HExtlib.dummy_floc))
    let mk_tactic tac = tac
    let apply_tactic tac = tac
    let goals (_, opened, closed) = opened, closed
-   let set_goals (opened, closed) (status, _, _) = (status, opened, closed)
    let get_stack (status, _) = GrafiteTypes.get_stack status
    
-   let get_status (status, goal) =
-      match status.GrafiteTypes.proof_status with
-         | GrafiteTypes.Incomplete_proof incomplete -> incomplete.GrafiteTypes.proof, goal
-        | _                              -> assert false
-      
-   let get_proof (status, _, _) =
-      match status.GrafiteTypes.proof_status with
-         | GrafiteTypes.Incomplete_proof incomplete -> incomplete.GrafiteTypes.proof
-        | _                              -> assert false
- 
    let set_stack stack (status, opened, closed) = 
      GrafiteTypes.set_stack stack status, opened, closed
  

diff --git a/helm/software/components/tactics/continuationals.ml b/helm/software/components/tactics/continuationals.ml
index 6bb419c03f9db57dcbeb6a69ba4f3d3d1b45642e..d90e100194538c483397485d061c908e3f6170ec 100644 (file)
--- a/helm/software/components/tactics/continuationals.ml
+++ b/helm/software/components/tactics/continuationals.ml
@@ -175,15 +175,10 @@ sig
   type output_status
 
   type tactic
-
-  val id_tactic : tactic
   val mk_tactic : (input_status -> output_status) -> tactic
   val apply_tactic : tactic -> input_status -> output_status
 
-  val get_status: input_status -> ProofEngineTypes.status
-  val get_proof: output_status -> ProofEngineTypes.proof
   val goals : output_status -> goal list * goal list (** opened, closed goals *)
-  val set_goals: goal list * goal list -> output_status -> output_status
   val get_stack : input_status -> Stack.t
   val set_stack : Stack.t -> output_status -> output_status
 

diff --git a/helm/software/components/tactics/continuationals.mli b/helm/software/components/tactics/continuationals.mli
index f9a17a9422ec389ca3e4c5aeff3bc36029289290..277dfe36296a468d44a548306d8e4941ce2351e8 100644 (file)
--- a/helm/software/components/tactics/continuationals.mli
+++ b/helm/software/components/tactics/continuationals.mli
@@ -79,15 +79,10 @@ sig
   type output_status
 
   type tactic
-
-  val id_tactic : tactic
   val mk_tactic : (input_status -> output_status) -> tactic
   val apply_tactic : tactic -> input_status -> output_status
 
-  val get_status: input_status -> ProofEngineTypes.status
-  val get_proof: output_status -> ProofEngineTypes.proof
   val goals : output_status -> goal list * goal list (** opened, closed goals *)
-  val set_goals: goal list * goal list -> output_status -> output_status
   val get_stack : input_status -> Stack.t
   val set_stack : Stack.t -> output_status -> output_status
 

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index eb3ebc1bba506c4a748b846d36a45a968fe814ec..63b8e12b59a362ddafa4deb855bf215ecf6db5be 100644 (file)
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -108,8 +108,6 @@ struct
 
   type tactic = PET.tactic
 
-  let id_tactic = id_tac
-
   (* f is an eval function of a machine;
      the machine is applied to a fresh stack and the final stack is read
      back to obtain the result of the tactic *)
@@ -130,12 +128,7 @@ struct
     let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
     (proof', opened_goals, closed_goals), stack
 
-  let get_status (status, _) = status
-  let get_proof ((proof, _, _), _) = proof
-
   let goals ((_, opened, closed), _) = opened, closed
-  let set_goals (opened, closed) ((proof, _, _), stack) =
-    (proof, opened, closed), stack
 
   (* Done only at the beginning of the eval of the machine *)
   let get_stack = snd