"the thesis becomes" now always performs a change.

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 242d6e3fe6476dab2d100f6253ea72d6d502215a..94ef66c952509257b70371333a5f9d3c6c990bbb 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -237,10 +237,12 @@ let case id ~params =
 
 let thesisbecomes t =
 let ty = None in
- (*BUG here: missing check on t *)
  match ty with
-    None -> Tacticals.id_tac
+    None ->
+     Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
+      (fun _ metasenv ugraph -> t,metasenv,ugraph)
   | Some ty ->
+     (*BUG here: missing check on t *)
      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
       (fun _ metasenv ugraph -> ty,metasenv,ugraph)
 ;;