Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion

is buggy in general.

1 files changed, 1 insertions, 1 deletions

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