aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.ml
AgeCommit message (Expand)Author
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-15Providing a centralized API for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
2018-10-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-11Merge PR #8161: Implement VERNAC EXTEND in coqppMaxime Dénès
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-02Pass unnamed arguments to ML macros.Pierre-Marie Pédrot
2018-09-19Fix #7754: universe declarations on mutual inductivesGaëtan Gilbert
2018-09-14Register: simpler syntaxVincent Laporte
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-13Add explicit atribute for template polymorphism.Gaëtan Gilbert
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-10Remove environment passing to coercion printersGaëtan Gilbert
2018-09-10Support for Local flag in Declare Scope, Undelimit/Delimit Scope, Bind Scope.Hugo Herbelin
2018-09-10Adding a command "Declare Scope" and deprecating scope implicit declaration.Hugo Herbelin
2018-09-06Merge PR #8295: Fix #8291: print universe names in universe context for Check.Matthieu Sozeau
2018-09-03Merge PR #7085: Turn the kernel reduction sharing flag into an argument passe...Maxime Dénès
2018-08-28Close #8091: print universe context for Eval when option on.Gaëtan Gilbert
2018-08-28Fix #8291: print universe names in universe context for Check.Gaëtan Gilbert
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.Pierre-Marie Pédrot
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-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] Generic syntax for flags/attributesVincent Laporte
2018-07-03[vernac] Add a “deprecated” attributeVincent Laporte
2018-07-03[vernac] mk_atts: an atts record with default valuesVincent Laporte
2018-07-03[vernac] attribute_of_flagsVincent Laporte
2018-07-01Add flag Uniform Inductive ParametersJasper Hugunin
2018-07-01Implement uniform parameters in ComInductiveJasper Hugunin
2018-06-28Make Environ.globals abstract.Gaëtan Gilbert
2018-06-24Handle mutual record at the vernac level.Pierre-Marie Pédrot
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-04Merge PR #7315: An attempt to clarify error message for Arguments needing "re...Maxime Dénès
2018-05-30Merge PR #7558: [api] Make `vernac/` self-contained.Maxime Dénès
2018-05-28Merge PR #7521: Fix soundness bug with VM/native and cofixpointsPierre-Marie Pédrot
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-27[tactics] Turn boolean locality hint parameter into a named one.Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-25An attempt to clarify error message for Arguments needing "rename" flag.Hugo Herbelin
2018-05-23[api] Move `Vernacexpr` to parsing.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 19:06:04 +0000