aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.ml
AgeCommit message (Expand)Author
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-30[declaremods] Remove abstraction of imperative module operationsEmilio Jesus Gallego Arias
2020-06-26[recLemmas] Nit on naming consistency.Emilio Jesus Gallego Arias
2020-06-26[declare] Return list of declared global in Proof.saveEmilio Jesus Gallego Arias
2020-06-26[declare] Merge remaining obligations bits into DeclareEmilio Jesus Gallego Arias
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[vernac] Nit refatoring on lemma command interpretationEmilio Jesus Gallego Arias
2020-06-26[declare] Use Recthm.t in mutual analysis functionsEmilio Jesus Gallego Arias
2020-06-26[declare] Refactor analysis and construction of mutual lemmasEmilio Jesus Gallego Arias
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] Refactor constant information into a record.Emilio Jesus Gallego Arias
2020-06-26[declare] Remove mutual internals from Info.t structure.Emilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-18[declare] Merge `DeclareObl` into `Declare`Emilio Jesus Gallego Arias
2020-05-18[obligations] Pre-functionalize Program stateEmilio Jesus Gallego Arias
2020-05-15Moving interpretation of Search commands to their own file: comSearch.ml.Hugo Herbelin
2020-05-15Cleaning the use of pstate and evar_map in Search.Hugo Herbelin
2020-05-15Search: Displaying the "use About" notice only when really needed.Hugo Herbelin
2020-05-15Addressing a suggestion from Théo Zimmermann.Hugo Herbelin
2020-05-15Search: new clauses for searching head, conclusion, kind...Hugo Herbelin
2020-05-15Renaming search_about_item into search_item.Hugo Herbelin
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...Hugo Herbelin
2020-05-14Generalize the interpretation of syntactic notation as reference to their head.Pierre-Marie Pédrot
2020-05-14Fixes #12234 (wrong environment for Show Proof).Hugo Herbelin
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-05-03[funind] Remove use of low-level entries in scheme generation.Emilio Jesus Gallego Arias
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-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-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
2020-04-13Partial import inductive(..)Gaëtan Gilbert
2020-04-13syntax for import filtersGaëtan Gilbert
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-30[ComDefinition] Split program from regular declarationsEmilio Jesus Gallego Arias
2020-03-30[lemma] Remove special case for first constant in mutual definition save path.Emilio Jesus Gallego Arias
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 03:08:27 +0000