coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-01-13	Make sure "Print Module" write a dot at the end of inductive definitions.	Guillaume Melquiond

2020-07-01	[state] Consolidate state handling in Vernacstate	Emilio Jesus Gallego Arias
	After #12504 , we can encapsulate and consolidate low-level state logic in `Vernacstate`, removing `States` which is now a stub. There is hope to clean up some stuff regarding the handling of low-level proof state, by moving both `Evarutil.meta_counter` and `Evd.evar_counter_summary` into the proof state itself [obligations state is taken care in #11836] , but this will take some time.
2020-06-30	[declaremods] Remove abstraction of imperative module operations	Emilio Jesus Gallego Arias
	Now that `Printmods` is above `Declaremods`, we don't need to pass the extra `mod_ops` argument.
2020-06-30	[states] Move States to vernac	Emilio Jesus Gallego Arias
	We continue to push state layers upwards, in preparation of a functional vernacular interpretation. Now we move `States` and `Printmod` which messes with the global state as to temporarily create envs with modules.