fixes coq#8190, code by Hugo Herbelin @herbelin

CohenCyril · Aug 2, 2018 · 1f41752 · 1f41752
1 parent eb50d7e
commit 1f41752
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
@@ -815,7 +815,7 @@ let () =
 let notation_subst bindings tac =
   let fold id c accu =
     let loc = Glob_ops.loc_of_glob_constr (fst c) in
-    let c = ConstrMayEval (ConstrTerm c) in
+    let c = TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_open_constr) c) in
     (make ?loc @@ Name id, c) :: accu
   in
   let bindings = Id.Map.fold fold bindings [] in