Commits on Aug 30, 2024

1. Typecheck the result of term unquotation. …

   In some cases, unquoting could generate terms that were ill-typed, typically
   when unquoting [I @hole] for some template polymorphic inductive type [I].
   Similarly universe levels were not computed at all, which could have led
   to bizarre failures.
   
   To ensure that the unquoted term makes sense at all, we simply perform a
   call to Typing before returning it. This has a non-trivial cost but since
   building the term is already linear, this should not hopefully matter that
   much in practice.

   

   ppedrot committed Aug 30, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 7bfa901
   • Browse repository at this point

   Copy the full SHA

   7bfa901 View commit details

   Browse the repository at this point in the history