feat: Update CoreM options from parsed header #177

Merged
aniva merged 5 commits from frontend/env-init into dev 2025-03-28 18:56:22 -07:00
Owner

This ensures open statements persist in both frontend.process context and any elaboration context.

  • refactor: Remove CoreM from MainM
  • refactor: Now GoalState's restore functions will additionally restore the name generator and macro scopes. This will be critical for future branch unification.
  • chore: Remove unncessary Elab.Term.synthesizeSyntheticMVarsNoPostponing call in GoalState.step
This ensures `open` statements persist in both `frontend.process` context and any elaboration context. - refactor: Remove `CoreM` from `MainM` - refactor: Now `GoalState`'s restore functions will additionally restore the name generator and macro scopes. This will be critical for future branch unification. - chore: Remove unncessary `Elab.Term.synthesizeSyntheticMVarsNoPostponing` call in `GoalState.step`
aniva added this to the 0.3 milestone 2025-03-17 19:15:21 -07:00
aniva added the
part/Frontend
part/REPL
part/Environment
category
feature
labels 2025-03-17 19:15:21 -07:00
aniva self-assigned this 2025-03-17 19:15:21 -07:00
aniva added a new dependency 2025-03-17 19:27:08 -07:00
aniva added 1 commit 2025-03-24 17:48:11 -07:00
aniva added 1 commit 2025-03-25 12:27:49 -07:00
aniva added 1 commit 2025-03-28 00:51:01 -07:00
aniva added 1 commit 2025-03-28 00:56:28 -07:00
aniva added a new dependency 2025-03-28 00:57:13 -07:00
Author
Owner

Need to write some tests to prevent regression, and this will be good to go.

Need to write some tests to prevent regression, and this will be good to go.
aniva added 1 commit 2025-03-28 18:46:25 -07:00
aniva merged commit 48485a868b into dev 2025-03-28 18:56:22 -07:00
aniva deleted branch frontend/env-init 2025-03-28 18:56:22 -07:00
Sign in to join this conversation.
No description provided.