Inverters/Inversion:

[helm.git] / helm / software / components / cic_acic / eta_fixing.ml

diff --git a/helm/software/components/cic_acic/eta_fixing.ml b/helm/software/components/cic_acic/eta_fixing.ml
index 78789179f8c739e84c7c29abdaef003cc0f67731..9ebd48b8b05f2233b72dc741f098e92ebc61f407 100644 (file)
--- a/helm/software/components/cic_acic/eta_fixing.ml
+++ b/helm/software/components/cic_acic/eta_fixing.ml
@@ -84,7 +84,8 @@ let rec fix_lambdas_wrt_type ty te =
       let t2 = 
          match t' with
            C.Appl l -> 
-             C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+             C.LetIn (C.Name "w",t',assert false,
+              C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
          | _ -> C.Appl (t'::(mk_rels no_sources 0)) in
       List.fold_right
         (fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2
@@ -145,7 +146,9 @@ let fix_according_to_type ty hd tl =
               (* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
               C.LetIn 
                 (C.Name "H", 
-                  C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
+                  C.Appl res,
+                   assert false,
+                    C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
     else 
       let name,source,target =
         (match ty with
@@ -199,15 +202,16 @@ let eta_fix metasenv context t =
    | C.Lambda (n,s,t) -> 
        C.Lambda 
         (n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
-   | C.LetIn (n,s,t) -> 
+   | C.LetIn (n,s,ty,t) -> 
        C.LetIn 
-        (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
+        (n,eta_fix' context s,eta_fix' context ty,
+          eta_fix' ((Some (n,(C.Def (s,ty))))::context) t)
    | C.Appl [] -> assert false 
    | C.Appl (he::tl) -> 
        let tl' =  List.map (eta_fix' context) tl in 
        let ty,_ = 
          CicTypeChecker.type_of_aux' metasenv context he 
-           CicUniv.empty_ugraph 
+           CicUniv.oblivion_ugraph 
        in
        fix_according_to_type ty (eta_fix' context he) tl'
 (*
@@ -236,7 +240,7 @@ let eta_fix metasenv context t =
        let term' = eta_fix' context term in
        let patterns' = List.map (eta_fix' context) patterns in
        let inductive_types,noparams =
-        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
            (match o with
                Cic.Constant _ -> assert false
              | Cic.Variable _ -> assert false
@@ -257,7 +261,7 @@ let eta_fix metasenv context t =
           else 
            let term_type,_ = 
               CicTypeChecker.type_of_aux' metasenv context term
-               CicUniv.empty_ugraph 
+               CicUniv.oblivion_ugraph 
             in
             (match term_type with
                C.Appl (hd::params) -> 
@@ -296,7 +300,7 @@ let eta_fix metasenv context t =
       (fun newsubst (uri,t) ->
         let t' = eta_fix' context t in
         let ty =
-         let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+         let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
             match o with
                Cic.Variable (_,_,ty,_,_) -> 
                  CicSubstitution.subst_vars newsubst ty