aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 20:39:15 +0000