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.

1 files changed, 12 insertions, 4 deletions

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)