Patch to add a debugging string to HExtlib.split_nth reverted

[helm.git] / helm / software / components / tactics / destructTactic.ml

diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml
index a8bfc007d42ac395c2c5995686bc6cbc181daf33..f6fb61ac1ddf0e4a5511cf4c639bcc0bb0d17423 100644 (file)
--- a/helm/software/components/tactics/destructTactic.ml
+++ b/helm/software/components/tactics/destructTactic.ml
@@ -92,7 +92,7 @@ let discriminate_tac ~term =
  let mk_branches_and_outtype turi typeno consno context args =
     (* a list of "True" except for the element in position consno which
      * is "False" *)
-    match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+    match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
     | C.InductiveDefinition (ind_type_list,_,paramsno,_)  ->
         let _,_,rty,constructor_list = List.nth ind_type_list typeno in 
         let false_constr_id,_ = List.nth constructor_list (consno - 1) in
@@ -158,7 +158,7 @@ let discriminate_tac ~term =
   let _,metasenv,_subst,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let termty,_ = 
-    CTC.type_of_aux' metasenv context term CU.empty_ugraph
+    CTC.type_of_aux' metasenv context term CU.oblivion_ugraph
   in
   match termty with
    | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
@@ -226,7 +226,7 @@ let clear_term first_time lterm =
       let (proof, goal) = status in
       let _,metasenv,_subst,_,_, _ = proof in
       let _,context,_ = CicUtil.lookup_meta goal metasenv in
-      let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+      let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
       debug_print (lazy ("\nclear di: " ^ pp context term));
       debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); 
       let g () = if first_time then raise exn_nothingtodo else T.id_tac in
@@ -277,9 +277,9 @@ let injection_tac ~lterm ~i ~continuation ~recur =
    * del costruttore *)
   let _,metasenv,_subst,_,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+  let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
   let termty,_ =
-    CTC.type_of_aux' metasenv context term CU.empty_ugraph
+    CTC.type_of_aux' metasenv context term CU.oblivion_ugraph
   in
   debug_print (lazy ("\ninjection su : " ^ pp context termty)); 
   match termty with (* an equality *)
@@ -301,9 +301,9 @@ let injection_tac ~lterm ~i ~continuation ~recur =
             List.nth applist1 (pred i),List.nth applist2 (pred i),consno2
         | _ -> assert false
       in
-      let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in
+      let tty',_ = CTC.type_of_aux' metasenv context t1' CU.oblivion_ugraph in
       let patterns,outtype =
-        match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+        match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
         | C.InductiveDefinition (ind_type_list,_,paramsno,_)->
            let left_params, right_params = HExtlib.split_nth paramsno params in
            let _,_,_,constructor_list = List.nth ind_type_list typeno in
@@ -383,7 +383,7 @@ let injection_tac ~lterm ~i ~continuation ~recur =
       let go_on =
         try
           let _,g = CTC.type_of_aux' metasenv context  cutted
-            CU.empty_ugraph
+            CU.oblivion_ugraph
           in
           let _,g = CTC.type_of_aux' metasenv context changed g in
           fst (CR.are_convertible ~metasenv context  t1' changed g)
@@ -442,7 +442,7 @@ let subst_tac ~lterm ~direction ~where ~continuation ~recur =
       let (proof, goal) = status in
       let _,metasenv,_subst,_,_, _ = proof in
       let _,context,_ = CicUtil.lookup_meta goal metasenv in
-      let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+      let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
       debug_print (lazy ("\nsubst " ^ (match direction with `LeftToRight -> "->" | `RightToLeft -> "<-") ^ " di: " ^ pp context term));
       let tactic = match where with
          | None      -> 
@@ -463,18 +463,18 @@ let subst_tac ~lterm ~direction ~where ~continuation ~recur =
 
 let rec destruct ~first_time lterm =
  let are_convertible hd1 hd2 metasenv context = 
-   fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
+   fst (CR.are_convertible ~metasenv context hd1 hd2 CU.oblivion_ugraph)
  in
  let recur = destruct ~first_time:false in
  let destruct status = 
   let (proof, goal) = status in
   let _,metasenv,_subst, _,_, _ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+  let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
   let tactic = if not (first_time || exists context term) then T.id_tac else begin
      debug_print (lazy ("\ndestruct di: " ^ pp context term)); 
      debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
-     let termty,_ = CTC.type_of_aux' metasenv context term CU.empty_ugraph in
+     let termty,_ = CTC.type_of_aux' metasenv context term CU.oblivion_ugraph in
      debug_print (lazy ("\ndestruct su: " ^ pp context termty)); 
      let mk_lterm term c m ug =
         let distance = List.length c - List.length context in