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 7f1ec58359b728857fb4536258e7f33de7b934f1..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 =
@@ -596,19 +597,21 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
     function
        (k, e, _, C.Rel n, s) as config ->
         let config' =
-         try
-          Some (RS.from_env (List.nth e (n-1)))
-         with
-          Failure _ ->
-           try
-            begin
-             match List.nth context (n - 1 - k) with
-                None -> assert false
-              | Some (_,C.Decl _) -> None
-              | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[])
-            end
-           with
-            Failure _ -> None
+         if not delta then None
+         else
+          try
+           Some (RS.from_env (List.nth e (n-1)))
+          with
+           Failure _ ->
+            try
+             begin
+              match List.nth context (n - 1 - k) with
+                 None -> assert false
+               | Some (_,C.Decl _) -> None
+               | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[])
+             end
+            with
+             Failure _ -> None
         in
          (match config' with 
              Some (k',e',ens',t',s') -> reduce (k',e',ens',t',s'@s)
@@ -643,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
@@ -906,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) ->
@@ -1169,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))