Fixed inversion, which was broken by the last changes in the refiner.

[helm.git] / helm / software / components / ng_tactics / nInversion.ml

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 6fc9b2eee467bc9e15073e4cd3e94a0d354f0cef..627885cb743628ed01c7b8b2ec04d6122ed2f23f 100644 (file)
--- 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
 ;;