* 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.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 1149bfa3b7dd661a91e6f839c2f72d6911576377..f33d56e1b9ceedbe061db7cc7562046f7ab5b3e4 100644 (file)
--- 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 *)