aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.ml
Commit message (Expand)AuthorAge
* Merge PR #6405: Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-29
|\
| * Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
* | [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
|/
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* Merge PR #6419: [vernac] Split `command.ml` into separate files.Gravatar Maxime Dénès2017-12-18
|\
| * [flags] Make program_mode a parameter for commands in vernac.Gravatar Emilio Jesus Gallego Arias2017-12-17
| * [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-12-17
* | Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.Gravatar Maxime Dénès2017-12-13
|\ \
| * | Fix anomaly in [Type foo] command, + print uctx like Check.Gravatar Gaëtan Gilbert2017-12-11
| |/
* / [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
|/
* [vernac] Couple of tweaks missing from previous PRs.Gravatar Emilio Jesus Gallego Arias2017-12-04
* Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona...Gravatar Maxime Dénès2017-12-01
|\
* \ Merge PR #1049: Remove obsolete localityGravatar Maxime Dénès2017-11-30
|\ \
* \ \ Merge PR #6244: [lib] [api] Introduce record for `object_prefix`Gravatar Maxime Dénès2017-11-30
|\ \ \
| | * | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| |/ / |/| |
| * | [lib] [api] Introduce record for `object_prefix`Gravatar Emilio Jesus Gallego Arias2017-11-29
| | * [proof] [api] Rename proof types in preparation for functionalization.Gravatar Emilio Jesus Gallego Arias2017-11-29
| |/ |/|
* | Merge PR #6199: [vernac] Uniformize type of vernac interpretation.Gravatar Maxime Dénès2017-11-29
|\ \
* \ \ Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \ | |_|/ |/| |
| | * [vernac] Adjust `interp` to pass polymorphic in the attributes.Gravatar Emilio Jesus Gallego Arias2017-11-27
| | * [vernac] Add polymorphic to the type of vernac interpration options.Gravatar Emilio Jesus Gallego Arias2017-11-27
| | * [vernac] Start to uniformize type of vernac interpretation.Gravatar Emilio Jesus Gallego Arias2017-11-27
| |/ |/|
* | Merge PR #6241: [lib] Generalize Control.timeout type.Gravatar Maxime Dénès2017-11-27
|\ \
* \ \ Merge PR #6041: Protecting the printing of filenames with spaceGravatar Maxime Dénès2017-11-27
|\ \ \
| | | * Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
| | * | [lib] Generalize Control.timeout type.Gravatar Emilio Jesus Gallego Arias2017-11-24
| |/ / |/| |
| | * Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
| |/ |/|
* | Merge PR #6197: [plugin] Remove LocalityFixme über hack.Gravatar Maxime Dénès2017-11-24
|\ \
| | * 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
| |/ |/|