From 8d3fd3aa8029fa7c5acb3118846cf18ffe752b9c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 5 May 2015 13:21:04 +0200
Subject: Fix bug #4212, congruence forgetting about some universe constraints.

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

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 05f4c49030..9952cb0807 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -253,6 +253,12 @@ let new_app_global f args k =
 
 let new_refine c = Proofview.V82.tactic (refine c)
 
+let assert_before n c =
+  Proofview.Goal.enter begin fun gl ->
+    let evm, _ = Tacmach.New.pf_apply e_type_of gl c in
+      Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
+  end
+    
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter begin fun gl ->
   let type_of t = Tacmach.New.pf_type_of gl t in
-- 
cgit v1.2.3