From 6add354ad9ca0f68d3ef311c4e53ee96d9fdb4d7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 22:46:05 +0200
Subject: Ensuring proper cast invariants in EConstr.kind.

The kernel does fishy things with casts, such that ensuring there are no
two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr
view as well.
---
 engine/eConstr.ml | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index f50a8b8501..9026800f2b 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -41,10 +41,11 @@ let safe_evar_value sigma ev =
 
 let rec whd_evar sigma c =
   match Constr.kind c with
-  | Evar (evk, args) ->
-    (match safe_evar_value sigma (evk, args) with
-        Some c -> whd_evar sigma c
-      | None -> c)
+  | Evar ev ->
+    begin match safe_evar_value sigma ev with
+    | Some c -> whd_evar sigma c
+    | None -> c
+    end
   | Sort (Type u) ->
     let u' = Evd.normalize_universe sigma u in
     if u' == u then c else mkSort (Sorts.sort_of_univ u')
@@ -64,6 +65,13 @@ let rec whd_evar sigma c =
     | None -> c
     | Some f -> whd_evar sigma (mkApp (f, args))
     end
+  | Cast (c0, k, t) when isEvar c0 ->
+    (** Enforce smart constructor invariant on casts. *)
+    let ev = destEvar c0 in
+    begin match safe_evar_value sigma ev with
+    | None -> c
+    | Some c -> whd_evar sigma (mkCast (c, k, t))
+    end
   | _ -> c
 
 let kind sigma c = Constr.kind (whd_evar sigma c)
-- 
cgit v1.2.3