From 9fea58122001535bdee63317b56f2afb727167c7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Feb 2015 14:05:16 +0100
Subject: Somehow fixing bug #3467.

The notations using tactics in term seem now not to respect globalized names.
It is not obvious that this is the expected behaviour, but at least it does
not die with an anomaly.
---
 tactics/tacsubst.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 42e61cb57e..afffaffbe9 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -27,9 +27,8 @@ let subst_quantified_hypothesis _ x = x
 
 let subst_declared_or_quantified_hypothesis _ x = x
 
-let subst_glob_constr_and_expr subst (c,e) =
-  assert (Option.is_empty e); (* e<>None only for toplevel tactics *)
-  (Detyping.subst_glob_constr subst c,None)
+let subst_glob_constr_and_expr subst (c, e) =
+  (Detyping.subst_glob_constr subst c, e)
 
 let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
 
-- 
cgit v1.2.3