From 3a841c391df854fa4397521d9bcd775a7804d84e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Nov 2006 16:50:15 +0000 Subject: [PATCH] "the thesis becomes" now always performs a change. --- helm/software/components/tactics/declarative.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index 242d6e3fe..94ef66c95 100644 --- 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) ;; -- 2.39.2