diff --git a/lib/gallinaGen.ml b/lib/gallinaGen.ml index a393c7b..fa11b94 100644 --- a/lib/gallinaGen.ml +++ b/lib/gallinaGen.ml @@ -133,6 +133,7 @@ let setup_coq () = (* for both definition we create dummy expressions that will never be used. * But according to the documentation the bodies of notations might be typechecked in the * future and this should work *) + let _ = !Flags.in_debugger in let dummy_eq = app_ (lambda_ [ binder_ [ "a"; "b" ] ] prop_) [ (ref_ "x"); (ref_ "y") ] in let () = Metasyntax.add_notation ~infix:false ~local:true None (Global.env ()) dummy_eq