From 18ff03b9480b4cc3fec155db743b37f3a4675509 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 25 Nov 2009 13:34:55 +0000 Subject: [PATCH] Fixed inversion, which was broken by the last changes in the refiner. --- .../components/ng_tactics/nInversion.ml | 20 +++++++++---------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index 6fc9b2eee..627885cb7 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -11,8 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -(*let pp m = prerr_endline (Lazy.force m);;*) -let pp _ = ();; +let pp m = prerr_endline (Lazy.force m);; +(* let pp _ = ();; *) let fresh_name = let i = ref 0 in @@ -132,7 +132,6 @@ let mk_inverter name it leftno ?selection outsort status baseuri = let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @ List.map mk_id hyplist @ CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in - let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def", 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some @@ -150,11 +149,10 @@ let mk_inverter name it leftno ?selection outsort status baseuri = let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem), CicNotationPt.Implicit (`Tagged "end")); CicNotationPt.Implicit (`Tagged "cut")] in - let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in - + let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in let status = NTactics.block_tac - (NTactics.branch_tac:: - NTactics.case_tac "inv":: + (NTactics.branch_tac :: + NTactics.case_tac "inv" :: (intros @ [NTactics.apply_tac ("",0,cut); NTactics.branch_tac; @@ -162,12 +160,12 @@ let mk_inverter name it leftno ?selection outsort status baseuri = NTactics.apply_tac ("",0,mk_id "Hcut"); NTactics.apply_tac ("",0,mk_id "refl_eq"); NTactics.shift_tac; - NTactics.case_tac "cut"; - NTactics.apply_tac ("",0,t) - (* ; + (*NTactics.case_tac "cut";*) + NTactics.apply_tac ("",0,t); NTactics.merge_tac; NTactics.merge_tac; - NTactics.skip_tac*)])) status in + NTactics.skip_tac])) status in + pp (lazy "inv 3"); status,status#obj ;; -- 2.39.2