From db37c9f3f32ae7a2abcd5e1a3f6239eddb5e1768 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 23 Jun 2014 13:01:31 +0200
Subject: Fix semantics of change p with c to typecheck c at each specific
 occurrence of p, avoiding unwanted universe constraints in presence of
 universe polymorphic constants. Fixing HoTT bugs # 36, 54 and 113.

---
 plugins/funind/recdef.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f141d3619c..38cbd0c533 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -668,7 +668,8 @@ let mkDestructEq :
      [Simple.generalize new_hyps;
       (fun g2 ->
 	change_in_concl None
-	  (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
+	  (fun env sigma -> 
+	    sigma, pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
 
-- 
cgit v1.2.3