From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 20 Apr 2007 11:30:44 +0000 (+0000)
Subject: Interface of the argument to Continuationals.Make greately simplified. The
X-Git-Tag: make_still_working~6372
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c175c78b4fd9d0bac50669e9954acf68d50014e7;p=helm.git

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 c93aeb654..f85c13bbb 100644
--- 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 6bb419c03..d90e10019 100644
--- 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 f9a17a942..277dfe362 100644
--- 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 eb3ebc1bb..63b8e12b5 100644
--- 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