Modifications to auto due to the introduction of the universe in

[helm.git] / components / tactics / declarative.ml

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 7561281a854ddd5871a32a577e7912a064517abd..fc8b175a273e04970d1af8dd2b32c97cb2ae5383 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -48,7 +48,7 @@ let suppose t id ty =
 let by_term_we_proved ~dbd t ty id ty' =
  let just =
   match t with
-     None -> Tactics.auto ~dbd ~params:[]
+     None -> Tactics.auto ~dbd ~params:[] (* da sistemare *) ~universe:Universe.empty
    | Some t -> Tactics.apply t
  in
   match id with
@@ -80,7 +80,7 @@ let by_term_we_proved ~dbd t ty id ty' =
 let bydone ~dbd t =
  let just =
   match t with
-     None -> Tactics.auto ~dbd ~params:[]
+     None -> Tactics.auto ~dbd ~params:[] ~universe:Universe.empty
    | Some t -> Tactics.apply t
  in
   just
@@ -150,8 +150,8 @@ let rewritingstep ~dbd lhs rhs just conclude =
    match just with
       None ->
        Tactics.auto ~dbd
-        ~params:["paramodulation","1"; "timeout","3"; "library","1"]
-    | Some just -> Tactics.apply just
+        ~params:["paramodulation","1"; "timeout","3"] ~universe:Universe.empty
+    | Some just -> Tactics.apply just 
   in
    match lhs with
       None ->