From 5c5f7c8d6a6ed8cbb99b12dde09fdbcc30ca8ab9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 22 May 2017 12:15:21 +0200
Subject: Compatibility fix while waiting for integration of Pierre Courtieu's
 PR #449.

---
 tactics/tactics.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e41236b1c3..fd10c622a0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2966,6 +2966,9 @@ let specialize (c,lbind) ipat =
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let sigma, term =
+    if lbind == NoBindings then
+      sigma, c
+    else
       let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
-- 
cgit v1.2.3