Procedural: we corrected two errors about the handling of mutcase (the "cases"

[helm.git] / helm / software / components / acic_procedural / proceduralConversion.ml

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index e42ad490eee970aee950dc98be1effcd0f0d99d1..97e32b94a458f1cdd3ce9bf9c49f30a21c5c675a 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -26,18 +26,16 @@
 module C    = Cic
 module E    = CicEnvironment
 module Un   = CicUniv
-module TC   = CicTypeChecker 
-module D    = Deannotate
+module TC   = CicTypeChecker
 module UM   = UriManager
 module Rd   = CicReduction
 module PEH  = ProofEngineHelpers
 module PT   = PrimitiveTactics
-
 module DTI  = DoubleTypeInference
 
-(* helpers ******************************************************************)
+module H    = ProceduralHelpers
 
-let cic = D.deannotate_term
+(* helpers ******************************************************************)
 
 let rec list_sub start length = function
    | _  :: tl when start  > 0 -> list_sub (pred start) length tl
@@ -61,7 +59,10 @@ let lift k n =
       | C.ARel (id, rid, m, b) as t -> 
          if m < k then t else 
         if m + n > 0 then C.ARel (id, rid, m + n, b) else
-        assert false
+        begin 
+           HLog.error (Printf.sprintf "ProceduralConversion.lift: %i %i" m n);
+           assert false
+        end
       | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss)
       | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss)
       | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss)
@@ -126,7 +127,7 @@ let clear_absts m =
       | C.ALambda (_, _, _, t) when n > 0  -> 
          aux 0 (pred n) (lift 1 (-1) t)
       | t                      when n > 0  ->
-           Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (cic t));
+           Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (H.cic t));
            assert false 
       | t                                  -> t
    in 
@@ -240,8 +241,8 @@ let clear c hyp =
    aux [] c
 
 let elim_inferred_type context goal arg using cpattern =
-   let metasenv, ugraph = [], Un.oblivion_ugraph in 
-   let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
+   let metasenv, ugraph = [], Un.default_ugraph in
+   let ety = H.get_type "elim_inferred_type" context using in
    let _splits, args_no = PEH.split_with_whd (context, ety) in
    let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim 
       ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no