Ajout du langage de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 6 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3af8748035..9e1698c25c 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -13,14 +13,9 @@ open Reduction
 open Instantiate
 open Type_errors
 open Proof_trees
+open Proof_type
 open Logic
 
-type 'a sigma = { 
-  it : 'a ; 
-  sigma : global_constraints }
-
-type validation = (proof_tree list -> proof_tree)
-type tactic = goal sigma -> (goal list sigma * validation)
 type transformation_tactic = proof_tree -> (goal list * validation)
 
 let hypotheses gl = gl.evar_env