"that is equivalent to" and "or equivalently" implemented in most situations.

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

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 50d4be88435e650976eda3fd9052f697bd87e0f1..370e326dbcd2f76fcda3efe06593f46e2ef0944c 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -34,27 +34,34 @@ let assume id t =
 ;;
 
 let suppose t id ty =
-(*BUG: ty not used *)
+(*BUG: check on t missing *)
+ let ty = match ty with None -> t | Some ty -> ty in
  Tacticals.then_
    ~start:
-       (Tactics.intros ~howmany:1
-             ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
+     (Tactics.intros ~howmany:1
+       ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
    ~continuation:
-            (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)  
-              (fun _ metasenv ugraph -> t,metasenv,ugraph))
+     (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)  
+      (fun _ metasenv ugraph -> ty,metasenv,ugraph))
 ;;
 
 let by_term_we_proved t ty id ty' =
-(*BUG: ty' not used *)
  match t with
     None -> assert false
   | Some t ->
-     Tacticals.thens
-     ~start:
-       (Tactics.cut ty
-         ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
-     ~continuations:
-       [ Tacticals.id_tac ; Tactics.apply t ]
+     let continuation =
+      match ty' with
+         None -> Tacticals.id_tac
+       | Some ty' ->
+          Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+          (fun _ metasenv ugraph -> ty,metasenv,ugraph)
+     in
+      Tacticals.thens
+      ~start:
+        (Tactics.cut ty
+          ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
+      ~continuations:
+        [ continuation ; Tactics.apply t ]
 ;;
 
 let bydone t =
@@ -65,12 +72,20 @@ let bydone t =
 ;;
 
 let we_need_to_prove t id ty =
-(*BUG: ty not used *)
  let aux status =
+  let cont,cutted =
+   match ty with
+      None -> Tacticals.id_tac,t
+    | Some ty ->
+       Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+        (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
   let proof,goals =
    ProofEngineTypes.apply_tactic
-    (Tactics.cut t
-      ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
+    (Tacticals.thens
+      ~start:
+       (Tactics.cut cutted
+         ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
+      ~continuations:[cont])
     status
   in
    let goals' =
@@ -197,8 +212,13 @@ let case id ~params =
 ;;
 
 let thesisbecomes t =
- (*BUG here: nothing done*)
- Tacticals.id_tac
+let ty = None in
+ (*BUG here: missing check on t *)
+ match ty with
+    None -> Tacticals.id_tac
+  | Some ty ->
+     Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
+      (fun _ metasenv ugraph -> ty,metasenv,ugraph)
 ;;
 
 let byinduction t id  = suppose t id None;;