aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-17Remove dead argument allow_old.Théo Zimmermann
2018-07-29Store marshallable data in the custom entry summary.Pierre-Marie Pédrot
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29Do not treat curly brackets specially in custom entries.Hugo Herbelin
2018-07-29Renaming ETName and ETReference so as to fit the user-visible terminology.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-26Merge PR #8050: Cleanup VERNAC EXTENDMaxime Dénès
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...Pierre-Marie Pédrot
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
2018-07-25Remove himsg.pr_puniverses, use @{} for universe printing in errorsMaxime Dénès
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-07-23Generate more compact escape sequences byJim
2018-07-19Merge PR #7941: Extend QuestionMark to produce a better error message in case...Pierre-Marie Pédrot
2018-07-17change into QuestionMark defaultSiddharth Bhat
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-07-13Remove useless libobject in proof_usingMaxime Dénès
2018-07-12Statically typecheck the VERNAC EXTEND wrapper.Pierre-Marie Pédrot
2018-07-12Export a wrapper simplifying the registration of vernacular commands.Pierre-Marie Pédrot
2018-07-11Merge PR #7898: Remove camlp4 remainsEmilio Jesus Gallego Arias
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-07-07Remove dead code that used to be there for CamlpX compatibility.Pierre-Marie Pédrot
2018-07-03fix syntax of .mlgVincent Laporte
2018-07-03[vernac] use a record for the contents of the “deprecated” attributeVincent Laporte
2018-07-03[vernac] use plain strings as attribute namesVincent Laporte
2018-07-03[vernac] indentationVincent Laporte
2018-07-03[vernac] Generic syntax for flags/attributesVincent Laporte
2018-07-03[vernac] Generic parsing rules for attributesVincent Laporte
2018-07-03[vernac] Add a “deprecated” attributeVincent Laporte
2018-07-03Allow “Let”-defined coercionsVincent Laporte
2018-07-03[vernac] Concrete syntax for attributesVincent Laporte
2018-07-03[vernac] mk_atts: an atts record with default valuesVincent Laporte
2018-07-03[vernac] attribute_of_flagsVincent Laporte
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-07-02Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points...Emilio Jesus Gallego Arias
2018-07-01Add flag Uniform Inductive ParametersJasper Hugunin
2018-07-01Implement uniform parameters in ComInductiveJasper Hugunin
2018-07-01[api] Fix wrong deprecation warning (#7915)Emilio Jesus Gallego Arias
2018-07-01Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Emilio Jesus Gallego Arias
2018-07-01Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break...Emilio Jesus Gallego Arias
2018-06-29Port g_vernac to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Port g_proofs to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Pierre-Marie Pédrot
2018-06-29Workaround to fix #7731 (printing not splitting line at break hint).Hugo Herbelin
2018-06-29Fixes #7712 (an anomaly in reporting bad recursive notation format).Hugo Herbelin
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 13:43:41 +0000