From 3c5ae672d701c15b24fba38f38f583ef9e7414af Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Jul 2007 20:19:24 +0000 Subject: [PATCH 1/1] Bug fixed: a ~with_cast is now inserted when appropriate to avoid translation of a bottom-up conversion into a top-down conversion. --- .../software/components/tactics/declarative.ml | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index b0615edb3..8e077c6bd 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -63,18 +63,24 @@ let by_term_we_proved ~dbd ~universe t ty id ty' = ~continuation:just ) | Some id -> - let continuation = + let ty',continuation = match ty' with - None -> Tacticals.id_tac + None -> ty,just | Some ty' -> - Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) - (fun _ metasenv ugraph -> ty',metasenv,ugraph) + ty', + Tacticals.then_ + ~start: + (Tactics.change + ~with_cast:true + ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) + (fun _ metasenv ugraph -> ty,metasenv,ugraph)) + ~continuation:just in Tacticals.thens ~start: - (Tactics.cut ty + (Tactics.cut ty' ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) - ~continuations:[ continuation ; just ] + ~continuations:[ Tacticals.id_tac ; continuation ] ;; let bydone ~dbd ~universe t = -- 2.39.2