From df1279b974ef4fc958d3ddb20b7416ea116d929c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Dec 2001 13:24:27 +0000
Subject: [PATCH] * Code improvement: there were two different functions both
 named eat_prods.   One has been renamed drop_prods. * Bug fix: decast was
 still too weak. Replaced by CicReduction.whd everywhere.

---
 .../cic_proof_checking/cicTypeChecker.ml      | 30 ++++++++-----------
 1 file changed, 12 insertions(+), 18 deletions(-)

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 1149bfa3b..f33d56e1b 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -463,12 +463,12 @@ and get_new_safes p c rl safes n nn x =
    | (C.Appl _, e, []) -> (e,safes,n,nn,x)
    | (_,_,_) -> raise (Impossible 7)
 
-and eat_prods n te =
+and drop_prods n te =
  let module C = Cic in
  let module R = CicReduction in
   match (n, R.whd te) with
      (0, _) -> te
-   | (n, C.Prod (_,_,ta)) when n > 0 -> eat_prods (n - 1) ta
+   | (n, C.Prod (_,_,ta)) when n > 0 -> drop_prods (n - 1) ta
    | (_, _) -> raise (Impossible 8)
 
 and eat_lambdas n te =
@@ -528,7 +528,7 @@ and check_is_really_smaller_arg n nn kl x safes te =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let cl' =
-                  List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
+                  List.map (fun (id,ty,r) -> (id, drop_prods paramsno ty, r)) cl
                  in
                   (isinductive,paramsno,cl')
              | _ ->
@@ -560,7 +560,7 @@ and check_is_really_smaller_arg n nn kl x safes te =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let cl' =
-                  List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
+                  List.map (fun (id,ty,r) -> (id, drop_prods paramsno ty, r)) cl
                  in
                   (isinductive,paramsno,cl')
              | _ ->
@@ -667,7 +667,7 @@ and guarded_by_destructors n nn kl x safes =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let cl' =
-                  List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
+                  List.map (fun (id,ty,r) -> (id, drop_prods paramsno ty, r)) cl
                  in
                   (isinductive,paramsno,cl')
              | _ ->
@@ -704,7 +704,7 @@ and guarded_by_destructors n nn kl x safes =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let cl' =
-                  List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
+                  List.map (fun (id,ty,r) -> (id, drop_prods paramsno ty, r)) cl
                  in
                   (isinductive,paramsno,cl')
              | _ ->
@@ -1042,7 +1042,7 @@ and type_of_aux' env t =
       let outsort = type_of_aux env outtype in
       let (need_dummy, k) =
        let rec guess_args t =
-        match decast t with
+        match CicReduction.whd t with
            C.Sort _ -> (true, 0)
          | C.Prod (_, s, t) ->
             let (b, n) = guess_args t in
@@ -1172,25 +1172,19 @@ and type_of_aux' env t =
         let (_,ty,_) = List.nth fl i in
          ty
 
- (* CSC: wrong name and position: decast really does Cast-LetIn reduction *)
- and decast =
-  let module C = Cic in
-   function
-      C.Cast (t,_) -> decast t
-    | C.LetIn (_,s,t) -> decast (CicSubstitution.subst s t)
-    | t -> t
-
  and sort_of_prod (t1, t2) =
   let module C = Cic in
-   match (decast t1, decast t2) with
+   let t1' = CicReduction.whd t1 in
+   let t2' = CicReduction.whd t2 in
+   match (t1', t2') with
       (C.Sort s1, C.Sort s2)
         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | (_,_) ->
       raise
-       (NotWellTyped ("Prod: sort1= " ^ CicPp.ppterm t1 ^ " ;
-         sort2= " ^ CicPp.ppterm t2))
+       (NotWellTyped
+        ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
 
  and eat_prods hetype =
   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
-- 
2.39.2