X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=fbb281c49d1467aa2ee753b866f308925111b56b;hb=7eb9140b9347edefbe859c4736187a9f5809c322;hp=833e1b1c4beed5c35bb7788e0520b6134d2a6715;hpb=f065a68682b23976d185370d85869c196da3f20b;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 833e1b1c4..fbb281c49 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -23,8 +23,6 @@
  * http://helm.cs.unibo.it/
  *)
 
-type location = int * int
-
 type direction = [ `Left | `Right ]
 type reduction_kind = [ `Reduce | `Simpl | `Whd ]
 type 'term pattern = Pattern of 'term
@@ -33,7 +31,7 @@ type 'term pattern = Pattern of 'term
   to the current goal *)
 
 type ('term, 'ident) tactic =
-  | LocatedTactic of location * ('term, 'ident) tactic
+  | LocatedTactic of CicAst.location * ('term, 'ident) tactic
 
   | Absurd
   | Apply of 'term
@@ -68,7 +66,7 @@ type ('term, 'ident) tactic =
   | Transitivity of 'term
 
 type 'tactic tactical =
-  | LocatedTactical of location * 'tactic tactical
+  | LocatedTactical of CicAst.location * 'tactic tactical
 
   | Fail
   | Do of int * 'tactic tactical