Skip to content

Commit

Permalink
enable in_debugger to avoid assertion error
Browse files Browse the repository at this point in the history
  • Loading branch information
yforster committed Jan 30, 2024
1 parent 17cf167 commit 6f511cf
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions lib/gallinaGen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 6f511cf

Please sign in to comment.