aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-04-05Fixes #11194 (Canonical/Coercion not located for coqdoc).Hugo Herbelin
2020-04-02Remove Chapter command.Théo Zimmermann
2020-04-01Merge PR #11306: Centralize the flag handling native compilation.Maxime Dénès
2020-04-01Merge PR #11945: Fix #11941: anomaly in equality schemesEmilio Jesus Gallego Arias
2020-03-31Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit ...Hugo Herbelin
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-31Remove check_hidden_implicit_parameters (not needed anymore)Gaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-31[proof] [stm] Force `opaque` in `close_future_proof`Emilio Jesus Gallego Arias
2020-03-31[proof] Split return_proof in partial and regular versions.Emilio Jesus Gallego Arias
2020-03-31[proof] Split delayed and regular proof closing functions, part IIEmilio Jesus Gallego Arias
2020-03-31Merge PR #11818: [proof] Further consolidation of the regular declaration pathGaëtan Gilbert
2020-03-31Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the gr...Maxime Dénès
2020-03-30[declare] [nit] Get `fix_exn` only in the case of an exception.Emilio Jesus Gallego Arias
2020-03-30[declare] Fuse prepare and declare for the non-interactive path.Emilio Jesus Gallego Arias
2020-03-30[lemmas] Minor tweak to Equations API.Emilio Jesus Gallego Arias
2020-03-30[program] Use common type for fixpoint declarations.Emilio Jesus Gallego Arias
2020-03-30[doc] [obligations] Some notes about `Program` implementationEmilio Jesus Gallego Arias
2020-03-30[classes] Declare obligation implicits using standard API.Emilio Jesus Gallego Arias
2020-03-30[declareDef] More consistent handling of universe bindersEmilio Jesus Gallego Arias
2020-03-30[declareObl] Remove hack w.r.t. to universe normalization.Emilio Jesus Gallego Arias
2020-03-30[obligations] Remove unnecessary ctx variableEmilio Jesus Gallego Arias
2020-03-30[declare] Make the type of closed entries opaque.Emilio Jesus Gallego Arias
2020-03-30[declareDef] Cleanup of allow_evars and check_evarsEmilio Jesus Gallego Arias
2020-03-30[declare] [obligations] Refactor preparation of obligation entryEmilio Jesus Gallego Arias
2020-03-30[ComDefinition] Split program from regular declarationsEmilio Jesus Gallego Arias
2020-03-30[lemmas] Cleanup in handling of mutual definitionsEmilio Jesus Gallego Arias
2020-03-30[lemmas] Remove workaround for non-uniform mutual bodyEmilio Jesus Gallego Arias
2020-03-30[comFixpoint] Minor cleanups in type declarations.Emilio Jesus Gallego Arias
2020-03-30[lemmas] [internal] Reify handling of mutual assumptionsEmilio Jesus Gallego Arias
2020-03-30[proof] Miscellaneous cleanup on proof info handlingEmilio Jesus Gallego Arias
2020-03-30[lemma] Remove special case for first constant in mutual definition save path.Emilio Jesus Gallego Arias
2020-03-31Merge PR #11647: [rfc] Consolidation of parsing interfacesPierre-Marie Pédrot
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Fix #11941: anomaly in equality schemesGaëtan Gilbert
2020-03-27Helping issue #11659 by leaving only the Cast hack in the grammar.Hugo Herbelin
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[gramlib] Remove warning function parameter in favor of standard mechanism.Emilio Jesus Gallego Arias
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
2020-03-25[declare] make restrict_ucontext an optional parameter.Emilio Jesus Gallego Arias
2020-03-25[lemmas] Use direct-style for mutual lemma declaration.Emilio Jesus Gallego Arias
2020-03-25[lemmas] Use direct-style for variable declaration.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize mutual per-entry informationEmilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize universe handling.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize mutual body construction.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize notation declaration.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 19:31:31 +0000