From a7917a32b24b652d2978a7aea171aa01da37eece Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 Apr 2016 10:55:38 +0200
Subject: Merging the ML tactic notation and plain Tactic Notation mechanisms.

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

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8baa668c7b..5e6a3eac73 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1126,7 +1126,7 @@ let type_uconstr ?(flags = constr_flags)
     ltac_constrs = closure.typed;
     ltac_uconstrs = closure.untyped;
     ltac_idents = closure.idents;
-    ltac_genargs = ist.Geninterp.lfun;
+    ltac_genargs = Id.Map.empty;
   } in
   let sigma = Sigma.to_evar_map sigma in
   let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
-- 
cgit v1.2.3