aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
Commit message (Expand)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
* Merge PR #7941: Extend QuestionMark to produce a better error message in case...Gravatar Pierre-Marie Pédrot2018-07-19
|\
| * change into QuestionMark defaultGravatar Siddharth Bhat2018-07-17
| * Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
* | Remove useless libobject in proof_usingGravatar Maxime Dénès2018-07-13
|/
* Merge PR #7898: Remove camlp4 remainsGravatar Emilio Jesus Gallego Arias2018-07-11
|\
| * Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-07-07
| * Remove dead code that used to be there for CamlpX compatibility.Gravatar Pierre-Marie Pédrot2018-07-07
* | fix syntax of .mlgGravatar Vincent Laporte2018-07-03
* | [vernac] use a record for the contents of the “deprecated” attributeGravatar Vincent Laporte2018-07-03
* | [vernac] use plain strings as attribute namesGravatar Vincent Laporte2018-07-03
* | [vernac] indentationGravatar Vincent Laporte2018-07-03
* | [vernac] Generic syntax for flags/attributesGravatar Vincent Laporte2018-07-03
* | [vernac] Generic parsing rules for attributesGravatar Vincent Laporte2018-07-03
* | [vernac] Add a “deprecated” attributeGravatar Vincent Laporte2018-07-03
* | Allow “Let”-defined coercionsGravatar Vincent Laporte2018-07-03
* | [vernac] Concrete syntax for attributesGravatar Vincent Laporte2018-07-03
* | [vernac] mk_atts: an atts record with default valuesGravatar Vincent Laporte2018-07-03
* | [vernac] attribute_of_flagsGravatar Vincent Laporte2018-07-03
|/
* Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\
* \ Merge PR #7703: Add an option to force parameters to be uniformGravatar Matthieu Sozeau2018-07-02
|\ \
| | * hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
| |/ |/|
* | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points...Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ \
| | * Add flag Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
| | * Implement uniform parameters in ComInductiveGravatar Jasper Hugunin2018-07-01
* | | [api] Fix wrong deprecation warning (#7915)Gravatar Emilio Jesus Gallego Arias2018-07-01
| |/ |/|
* | Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \
* \ \ Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break...Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ \
| | | * Port g_vernac to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | * Port g_proofs to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | * Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Gravatar Pierre-Marie Pédrot2018-06-29
| |_|/ |/| |
| * | Workaround to fix #7731 (printing not splitting line at break hint).Gravatar Hugo Herbelin2018-06-29
| | * Fixes #7712 (an anomaly in reporting bad recursive notation format).Gravatar Hugo Herbelin2018-06-29
| |/
* | Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Gravatar Maxime Dénès2018-06-29
|\ \
* | | Make Environ.globals abstract.Gravatar Gaëtan Gilbert2018-06-28
| |/ |/|
* | Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \
| | * Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| |/ |/|
* | Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\ \
* \ \ Merge PR #7906: universes_of_constr don't include universes of monomorphic co...Gravatar Pierre-Marie Pédrot2018-06-26
|\ \ \
* \ \ \ Merge PR #7775: Fix handling of universe context for expanded program obligat...Gravatar Maxime Dénès2018-06-26
|\ \ \ \
| | | * | Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |_|/ / |/| | |
| | * | universes_of_constr don't include universes of monomorphic constantsGravatar Gaëtan Gilbert2018-06-26
* | | | Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Gravatar Matthieu Sozeau2018-06-25
|\ \ \ \
* \ \ \ \ Merge PR #7559: Existing Class noop when already a class + warning.Gravatar Matthieu Sozeau2018-06-25
|\ \ \ \ \
| | | | | * Handle mutual record at the vernac level.Gravatar Pierre-Marie Pédrot2018-06-24
| |_|_|_|/ |/| | | |
* | | | | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
| |_|_|/ |/| | |
| | | * Fix handling of universe context for expanded program obligations.Gravatar Matthieu Sozeau2018-06-22
| |_|/ |/| |
| | * Remove hack skipping comparison of algebraic universes in subtyping.Gravatar Gaëtan Gilbert2018-06-22
| |/ |/|
* | Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\ \
* \ \ Merge PR #7801: [vernac] Add option to force building really mutual induction...Gravatar Enrico Tassi2018-06-19
|\ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-23 20:15:59 +0000