From 73663b52b3e1d8ed2f5936177bcc13b6e6b69997 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 Sep 2006 15:29:40 +0000 Subject: [PATCH] Bug fixed: "by ... we proved ... that is equivalent to ...": the is equivalent to part was not considered because of a stupid typo. --- helm/software/components/tactics/declarative.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index 4a7d3e52c..4dcf38b6d 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -55,8 +55,8 @@ let by_term_we_proved ~dbd t ty id ty' = 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) + Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) + (fun _ metasenv ugraph -> ty',metasenv,ugraph) in Tacticals.thens ~start: -- 2.39.2