attached auto

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index a7c7a9ae21329089fc0c3983ca8c6618a08b1a69..34b3d01e0cc18a72dde5f36c0953930b46989681 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -335,7 +335,8 @@ EXTEND
         TacticAst.Apply (loc, t)
     | [ IDENT "assumption" ] ->
         TacticAst.Assumption loc
-    | [ IDENT "auto" ] -> TacticAst.Auto loc
+    | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> 
+          TacticAst.Auto (loc,num)
     | [ IDENT "change" ];
       t1 = tactic_term; "with"; t2 = tactic_term;
       where = tactic_where ->

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index d4e94b28bea16ce511ca4341b6489378becedde4..23a8b8e6755c34071a78bdd1419a9ea5e6118808 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -38,7 +38,7 @@ type loc = CicAst.location
 type ('term, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
-  | Auto of loc
+  | Auto of loc * int option
   | Assumption of loc
   | Change of loc * 'term * 'term * 'ident option (* what, with what, where *)
   | Change_pattern of loc * 'term pattern * 'term * 'ident option

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 918e7bd71f15d13dcbaa893054e633fc34327b02..50a96d2addd5bb58d5f1bd7da44e32f4f8b02268 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -154,7 +154,7 @@ let rec auto dbd = function
 ;; 
 
 
-let auto_tac  ~(dbd:Mysql.dbd) =
+let auto_tac  ?num ~(dbd:Mysql.dbd) =
   let auto_tac dbh (proof,goal) =
   prerr_endline "Entro in Auto";
   match (auto dbd [(proof, [(goal,depth)],None)]) with

diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli
index 15ed54d1dd9da2f9912ef097464108ca7c15522e..0b5a9ca9b35d9dcae5b17d4a651263c09d6742d7 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.mli
+++ b/helm/ocaml/tactics/autoTactic.mli
@@ -24,5 +24,5 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val auto_tac : dbd:Mysql.dbd -> ProofEngineTypes.tactic
+val auto_tac : ?num:int option -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
 val auto_tac_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index d70c94ac54f39a057b0b4bb7d414bb2b35e0cccd..d8e02127df22bd8484b9d6c3519e962448ffda4c 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -2,7 +2,7 @@
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
-val auto : dbd:Mysql.dbd -> ProofEngineTypes.tactic
+val auto : ?num:int option -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
 val auto_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic
 val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
 val compare : term:Cic.term -> ProofEngineTypes.tactic