aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-06-08Merge PR #12480: Don't suggest Proof using when no section variablesEmilio Jesus Gallego Arias
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
2020-06-06Fix uncaught NotArity in inductive typeGaëtan Gilbert
2020-06-03[declare] Hide internals of variable declaration entries.Emilio Jesus Gallego Arias
2020-06-02Merge PR #11974: Require in Section: warning is now about fragility not depre...Emilio Jesus Gallego Arias
2020-05-29Merge PR #12393: [declare] Miscellaneous nits from my main dev treeGaëtan Gilbert
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-28Fixing compilation with -natdynlink no.Hugo Herbelin
2020-05-26[declare] Split univs_poly_private in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Factor common universe computation in close proof.Emilio Jesus Gallego Arias
2020-05-26[declare] Split univs_deferred in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Factor out universe computation in close_proofEmilio Jesus Gallego Arias
2020-05-26[declare] Nit on errors.Emilio Jesus Gallego Arias
2020-05-26[declare] Turn restrict_ucontext hack into an internal parameterEmilio Jesus Gallego Arias
2020-05-26[nit] Remove unused exported error message in obligationsEmilio Jesus Gallego Arias
2020-05-26[declare] Don't expose internal parameter oblsEmilio Jesus Gallego Arias
2020-05-26[declare] Simplify exported type of definition_entryEmilio Jesus Gallego Arias
2020-05-21Merge PR #12371: [obligations] Minor refactoringGaëtan Gilbert
2020-05-21Merge PR #12358: [topfmt] Set formatter + flush fixGaëtan Gilbert
2020-05-20[obligations] [nit] Refactor obligation printing.Emilio Jesus Gallego Arias
2020-05-20[obligations] `declare_obligation` now takes an `UState.t`Emilio Jesus Gallego Arias
2020-05-20[declare] [nit] Use proper type alias for in ProgramDecl interfaceEmilio Jesus Gallego Arias
2020-05-20[nit] Remove `Declare.Obls.err_not_transp`Emilio Jesus Gallego Arias
2020-05-20Merge PR #12356: [declare] Remove unused parameters in prepare_obligationGaëtan Gilbert
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
2020-05-19[declare] Remove unused parameters in prepare_obligationEmilio Jesus Gallego Arias
2020-05-19[declare] Minor tweaks in prepare_obligationEmilio Jesus Gallego Arias
2020-05-19[declare] Remove dead code in prepare_obligationEmilio Jesus Gallego Arias
2020-05-19[universes] [api] Provide UState.from_envEmilio Jesus Gallego Arias
2020-05-18[declare] Grand unification of the proof save path.Emilio Jesus Gallego Arias
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-18[search] [ssr] Emit deprecated message when calling search from ssreflectEmilio Jesus Gallego Arias
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
2020-05-15Deprecate SearchHead.Théo Zimmermann
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-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...Hugo Herbelin
2020-05-14Merge PR #12296: Fixes #12234: wrong environment for Show ProofGaëtan Gilbert
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
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-14Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.Gaëtan Gilbert
2020-05-14Merge PR #8808: Extending support for mixing binders and terms in abbreviationsEmilio Jesus Gallego Arias
2020-05-14Merge PR #12244: Store the OCaml version used for Coq in vo files.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 09:35:20 +0000