something was really too slow...

[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 0e063d82b6f60b728b4608715e8a80e75957cd05..8e077c6bd7e2d289f71763bbff9f183cbfd0a0d6 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -63,18 +63,24 @@ let by_term_we_proved ~dbd ~universe t ty id ty' =
             ~continuation:just
       )
    | Some id ->
-       let continuation =
+       let ty',continuation =
         match ty' with
-           None -> Tacticals.id_tac
+           None -> ty,just
          | Some ty' ->
-             Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
-              (fun _ metasenv ugraph -> ty',metasenv,ugraph)
+            ty',
+            Tacticals.then_
+             ~start:
+               (Tactics.change
+                 ~with_cast:true
+                 ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+                 (fun _ metasenv ugraph -> ty,metasenv,ugraph))
+             ~continuation:just
        in
         Tacticals.thens
         ~start:
-          (Tactics.cut ty
+          (Tactics.cut ty'
             ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
-        ~continuations:[ continuation ; just ]
+        ~continuations:[ Tacticals.id_tac ; continuation ]
 ;;
 
 let bydone ~dbd ~universe t =
@@ -184,7 +190,17 @@ 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 *)
+    | `Proof ->
+        Tacticals.id_tac
   in
    let plhs,prhs,prepare =
     match lhs with