aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
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
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
2020-05-13Centralize the OCaml version-checking function.Pierre-Marie Pédrot
2020-05-13Store the OCaml version used for Coq in vo files.Pierre-Marie Pédrot
2020-05-12Remove legacy Refiner error constructors.Pierre-Marie Pédrot
2020-05-12Do not use Unsafe.to_constr for old refiner conclusion.Pierre-Marie Pédrot
2020-05-11Merge PR #12129: Add a `with_strategy` tacticPierre-Marie Pédrot
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:03:07 +0000