From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 2 May 2005 13:58:45 +0000 (+0000)
Subject: attached auto
X-Git-Tag: single_binding~121
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2e5bbbe9aaae0b0d2b2ad7b91b17dbc25ec21929;p=helm.git

attached auto
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index a7c7a9ae2..34b3d01e0 100644
--- 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 d4e94b28b..23a8b8e67 100644
--- 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 918e7bd71..50a96d2ad 100644
--- 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 15ed54d1d..0b5a9ca9b 100644
--- 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 d70c94ac5..d8e02127d 100644
--- 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