many changes:

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

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 2f012ed40d9eded87bf8fcf62c6c0dd929aafac6..24801542dabcb76f57a6684a6d60fccaef31a488 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/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
@@ -257,7 +265,7 @@ let we_proceed_by_cases_on t pat =
 
 let we_proceed_by_induction_on t pat =
  let pattern = None, [], Some pat in
- Tactics.elim_intros ~depth:0 ~pattern t
+ Tactics.elim_intros ~depth:0 (*~pattern*) t
 ;;
 
 let case id ~params =