aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-05-09Merge PR #12241: [declare] Merge DeclareDef into DeclareGaëtan Gilbert
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-05-07[declare] Remove fix_exn internal access.Emilio Jesus Gallego Arias
2020-05-06Stop keeping outdated static list of keywords.Hugo Herbelin
2020-05-06Documenting plugin/tactic/stdlib keywords in corresponding chapters.Hugo Herbelin
2020-05-03[declare] Add deprecation notices for compat modules.Emilio Jesus Gallego Arias
2020-05-03[funind] Remove use of low-level entries in scheme generation.Emilio Jesus Gallego Arias
2020-05-01Changing fixpoint message "decreasing" -> "guarded".Hugo Herbelin
2020-05-01Warn when a (co)fixpoint is not truly recursive.Hugo Herbelin
2020-05-01Slight modification of the partial-order algorithm so that it does notHugo Herbelin
2020-04-30Merge PR #12216: Remove outdated code and comments in Declare.Emilio Jesus Gallego Arias
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
2020-04-30Remove outdated code and comments in Declare.Pierre-Marie Pédrot
2020-04-29Merge the call to tclEFFECTS into find_scheme.Pierre-Marie Pédrot
2020-04-29Remove dead user-facing code in scheme generation.Pierre-Marie Pédrot
2020-04-28Merge PR #12193: Close files in fetch_delayedEmilio Jesus Gallego Arias
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
2020-04-28Add comment about decide equality dependence computation.Pierre-Marie Pédrot
2020-04-28Return an option in lookup_scheme.Pierre-Marie Pédrot
2020-04-28Stop relying on side-effects for recursive scheme declaration.Pierre-Marie Pédrot
2020-04-28Close files in fetch_delayedGaëtan Gilbert
2020-04-27Do not delay the loading of the library_disk field when requiring libraries.Pierre-Marie Pédrot
2020-04-27Improve the Allow SProp error message.Théo Zimmermann
2020-04-26Open object files in binary mode.Pierre-Marie Pédrot
2020-04-26Move the ObjFile module to its own file.Pierre-Marie Pédrot
2020-04-26Implement a name-based representation for vo files.Pierre-Marie Pédrot
2020-04-25Fix recursively vs corecursively defined messageTej Chajed
2020-04-23Merge PR #12130: [declare] [tactics] Move declare to `vernac`Pierre-Marie Pédrot
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...Pierre-Marie Pédrot
2020-04-22Remove # keywords in PrimitivePierre Roux
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-21[declare] [compat] Add alias for deprecated functionEmilio Jesus Gallego Arias
2020-04-21[nit] Remove useless indirect alias.Emilio Jesus Gallego Arias
2020-04-21[declare] Remove `declare_private_constant` from the public API.Emilio Jesus Gallego Arias
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-04-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias
2020-04-20Move new iter_table function to Goptions.Théo Zimmermann
2020-04-20Use polymorphic record for Vernacentries.iter_tableGaëtan Gilbert
2020-04-20Improve undeclared key messages.Théo Zimmermann
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables (incid...Lysxia
2020-04-17Merge PR #11135: Simplifying the code declaring the constants bound to primit...Pierre-Marie Pédrot
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-16Merge PR #11982: Fix #11854 error message on unsolved evars in Instance.Pierre-Marie Pédrot
2020-04-16Merge PR #12101: Add needed commas in messageGaëtan Gilbert
2020-04-15Add needed commas in messageJim Fehrle
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:59:28 +0000