aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.ml
Commit message (Expand)AuthorAge
...
| | * Quote file names which have spaces in "Print LoadPath".Gravatar Hugo Herbelin2017-11-23
| |/ |/|
| * [plugin] Encapsulate modifiers to vernac commands.Gravatar Emilio Jesus Gallego Arias2017-11-22
* | [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Maxime Dénès2017-11-21
|\
* | [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| * [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
|/
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Merge PR #6063: Finish removing Show Goal uidGravatar Maxime Dénès2017-11-06
|\
| * Finish removing Show Goal uidGravatar Gaëtan Gilbert2017-11-04
* | provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesGravatar Matej Košík2017-11-01
|/
* Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Gravatar Maxime Dénès2017-10-20
|\
* | [vernac] [state] Cache freeze/unfreezeGravatar Emilio Jesus Gallego Arias2017-10-17
* | [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* | [stm] Move interpretation state to VernacentriesGravatar Emilio Jesus Gallego Arias2017-10-17
* | Code factorization Vernacentries.interp on VernacProof.Gravatar Gaëtan Gilbert2017-10-10
* | [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
| * Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05
* | Implementing a generic mechanism for locating named objects from Coq side.Gravatar Pierre-Marie Pédrot2017-10-03
* | Merge PR #1040: Efficient fresh name generationGravatar Maxime Dénès2017-10-03
|\ \
* | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| |/ |/|
| * Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\
* \ Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \
* | | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
| * | Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
|/ /
| * Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
|/
* Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...Gravatar Maxime Dénès2017-09-15
|\
* | Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
* | Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
| * [vernac] Store Infix Modifier in Vernac Notation.Gravatar Pierre-Marie Pédrot2017-08-29
|/
* Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
* Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\
* \ Merge PR #919: Remove a few useless evar-normalizations in printing code.Gravatar Maxime Dénès2017-08-01
|\ \
| | * Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
| | * Change the option for cumulativityGravatar Amin Timany2017-07-31
| | * Issue error on monomorphic cumulative inductivesGravatar Amin Timany2017-07-31
* | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \ | |_|/ |/| |
| * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | * Remove a few useless evar-normalizations in printing code.Gravatar Pierre-Marie Pédrot2017-07-26
| |/
* / Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
|/
* Merge PR #770: [proof] Move bullets to their own module.Gravatar Maxime Dénès2017-07-19
|\
* | Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* | [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
* | Remove Warnings: unused value ...Gravatar Amin Timany2017-06-16
* | Change the option to Set Inductive CumulativityGravatar Amin Timany2017-06-16
* | Correct coqchk reductionGravatar Amin Timany2017-06-16
* | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16