ancient graph regarding universes and trust=false, universes calculated for internal...

[helm.git] / helm / software / components / cic_proof_checking / cicReduction.ml

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 532d0dc1ec374f20a0b135cbedc8495e4767f827..11fd5123560b1f411bd8a77832c30a6db7150f01 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -451,7 +451,8 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,
        | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
        | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
        | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
-       | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
+       | C.LetIn (n,s,ty,t) ->
+          C.LetIn (n, unwind_aux m s, unwind_aux m ty, unwind_aux (m + 1) t)
        | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
        | C.Const (uri,exp_named_subst) ->
           let params =
@@ -645,7 +646,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
      | (_, _, _, C.Lambda _, []) as config -> config
      | (k, e, ens, C.Lambda (_,_,t), p::s) ->
          reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
-     | (k, e, ens, C.LetIn (_,m,t), s) ->
+     | (k, e, ens, C.LetIn (_,m,_,t), s) ->
         let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
          reduce (k+1, m'::e, ens, t, s)
      | (_, _, _, C.Appl [], _) -> assert false
@@ -908,17 +909,21 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
+           let b',ugraph' = aux true context s1 s2 ugraph in
            if b' then
              aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
                t1 t2 ugraph'
            else
              false,ugraph
-        | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
+        | (C.LetIn (name1,s1,ty1,t1), C.LetIn(_,s2,ty2,t2)) ->
            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
            if b' then
-            aux test_equality_only
-             ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
+            let b',ugraph = aux test_equality_only context ty1 ty2 ugraph in
+            if b' then
+             aux test_equality_only
+              ((Some (name1, (C.Def (s1,ty1))))::context) t1 t2 ugraph'
+            else
+              false,ugraph
            else
              false,ugraph
         | (C.Appl l1, C.Appl l2) ->
@@ -1171,7 +1176,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term =
   | C.Lambda (n,s,t) -> 
       let s' = aux ctx s in
       C.Lambda (n, s', aux ((decl n s')::ctx) t)
-  | C.LetIn (n,s,t) ->
+  | C.LetIn (n,s,_,t) ->
       (* the term is already in weak head normal form *)
       assert false
   | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))