added command and script ASTs with _debugging_only_ pretty printers

[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 833e1b1c4beed5c35bb7788e0520b6134d2a6715..fbb281c49d1467aa2ee753b866f308925111b56b 100644 (file)
--- 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