From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 27 Nov 2006 16:50:15 +0000 (+0000)
Subject: "the thesis becomes" now always performs a change.
X-Git-Tag: 0.4.95@7852~769
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d738a2c22023d2f6df4c60faf4dd18eb1a8ad970;p=helm.git

"the thesis becomes" now always performs a change.
---

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 242d6e3fe..94ef66c95 100644
--- a/components/tactics/declarative.ml
+++ b/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)
 ;;