many changes:

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

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 0e063d82b6f60b728b4608715e8a80e75957cd05..24801542dabcb76f57a6684a6d60fccaef31a488 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -184,7 +184,15 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
           Tacticals.first
            [Tactics.auto ~dbd ~params ~universe ;
             Tactics.auto ~dbd ~params:params' ~universe]
-    | `Term just -> Tactics.apply just 
+    | `Term just -> 
+         let ty,_ =
+           CicTypeChecker.type_of_aux' metasenv context just
+             CicUniv.empty_ugraph         
+         in
+          Tactics.solve_rewrite 
+              ~universe:(Universe.index Universe.empty 
+                 (Universe.key ty) just) ~steps:1 ()
+         (* Tactics.apply just *)
   in
    let plhs,prhs,prepare =
     match lhs with