From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 20:09:26 +0100
Subject: Eliminating parts of the right-hand side compatibility layer

---
 plugins/cc/cctac.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a12ef00ec3..6295e004e1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -87,6 +87,7 @@ let rec decompose_term env sigma t=
 	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->
        let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in
+       let t = EConstr.Unsafe.to_constr t in
        if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
-- 
cgit v1.2.3