From a181bcb8d8050984e57f4a21cc7e97c043feb043 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 5 Nov 2018 15:18:16 +0100
Subject: Add a check that the return stack of an FProd is indeed empty.

---
 kernel/typeops.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a87355e927..c9acd168e8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -151,6 +151,11 @@ let type_of_abstraction _env name var ty =
 let make_judgev c t = 
   Array.map2 make_judge c t
 
+let rec check_empty_stack = function
+| [] -> true
+| CClosure.Zupdate _ :: s -> check_empty_stack s
+| _ -> false
+
 let type_of_apply env func funt argsv argstv =
   let open CClosure in
   let len = Array.length argsv in
@@ -159,7 +164,9 @@ let type_of_apply env func funt argsv argstv =
   let rec apply_rec i typ =
     if Int.equal i len then term_of_fconstr typ
     else
-      let typ, _ = whd_stack infos tab typ [] in
+      let typ, stk = whd_stack infos tab typ [] in
+      (** The return stack is known to be empty *)
+      let () = assert (check_empty_stack stk) in
       match fterm_of typ with
       | FProd (_, c1, c2, e) ->
         let arg = argsv.(i) in
-- 
cgit v1.2.3