From b30ca8ac9e0225e6505fea0004ea37e7649c9cb6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 3 Nov 2015 17:25:49 -0500
Subject: Fix bug in proofs/logic.ml
 type_of_global_reference_knowing_conclusion is buggy in general.

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7756553e2d..2a46efd8ef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3329,7 +3329,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 	if defined then Some c', typ_of ctxenv !sigma c'
 	else None, c'
       in
-      let term = make_abstract_generalize gl id concl dep ctx body c' eqs args refls in
+      let term = make_abstract_generalize {gl with sigma = !sigma} id concl dep ctx body c' eqs args refls in
 	Some (term, !sigma, dep, succ (List.length ctx), vars)
     else None
 
-- 
cgit v1.2.3