aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-07[declare] Remove fix_exn internal access.Emilio Jesus Gallego Arias
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-07Remove call to Refiner API from Funind.Pierre-Marie Pédrot
2020-05-07Port Evar_tactics to the new API.Pierre-Marie Pédrot
2020-05-07Merge PR #12236: [funind] Remove use of low-level entries in scheme generation.Gaëtan Gilbert
2020-05-07Merge PR #12262: Fix #12211 (TIMED for ocaml files doesn't print file name)Gaëtan Gilbert
2020-05-07Merge PR #12024: Fixes for LaTeX/html export of standard library in coqdocThéo Zimmermann
2020-05-07[win] rules to build ElpiEnrico Tassi
2020-05-07[win] bump camlp5 to 7.11 since OCaml 4.08 requires itEnrico Tassi
2020-05-07[win] since 4.07 the seq package is part of ocamlEnrico Tassi
2020-05-07[win] Coq trunk is now called masterEnrico Tassi
2020-05-07Cleanup formatting in .. coqtop:: directivesQuentin Carbonneaux
2020-05-07Merge PR #12267: [ci] bump elpi to 1.11Emilio Jesus Gallego Arias
2020-05-07Documenting the new behavior of "subst".Hugo Herbelin
2020-05-07Adding change log for #12146.Hugo Herbelin
2020-05-07Tactic subst now inactive on section variables occurring indirectly in goal.Hugo Herbelin
2020-05-07Termops: Adding functions local_occur_var_in_decl and occur_var_indirectly.Hugo Herbelin
2020-05-07Drop some the coqtop output, rephrase a bitQuentin Carbonneaux
2020-05-07[ci] overlay for coq-elpiEnrico Tassi
2020-05-07Export API to recover values out of Ltac application.Pierre-Marie Pédrot
2020-05-07Add helper API to define low-level Ltac functions.Pierre-Marie Pédrot
2020-05-06Add an example to motivate strictly positive occurrences checkQuentin Carbonneaux
2020-05-06Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann.Hugo Herbelin
2020-05-06Merge PR #12171: [stdlib] [list] Symmetry in conclusions of map_eq_cons and m...Hugo Herbelin
2020-05-06[ci] bump elpi to 1.11Enrico Tassi
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
2020-05-06Merge PR #12018: Adding properties about implb in Bool.vAnton Trunov
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
2020-05-06Fix #12211Jason Gross
2020-05-06Layout of Bool.v, especially for coqdoc.Hugo Herbelin
2020-05-06Adding properties about implb.Hugo Herbelin
2020-05-06Moving lazymatch and multimatch to simple identifiers.Hugo Herbelin
2020-05-06Stop keeping outdated static list of keywords.Hugo Herbelin
2020-05-06Mention keywords from g_ltac.mlg used in Ltac.Hugo Herbelin
2020-05-06Mention keywords used in tactics from g_tactic.mlg.Hugo Herbelin
2020-05-06Documenting plugin/tactic/stdlib keywords in corresponding chapters.Hugo Herbelin
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
2020-05-05Merge PR #12252: [refman] Add missing (only parsing) to example of compat not...Clément Pit-Claudel
2020-05-05Fix GeoCoq slowdown.Pierre-Marie Pédrot
2020-05-05[refman] Add missing (only parsing) to example of compat notations.Théo Zimmermann
2020-05-05[ssr] wrap a couple of exception with tclLIFTEnrico Tassi
2020-05-04[ssr] get rid of (pf_)mkSsrConstEnrico Tassi
2020-05-04Merge PR #12225: [ci] [doc] More detailed documentation for overlay buildingThéo Zimmermann
2020-05-04update documentation for overlay buildingOlivier Laurent
2020-05-04Merge PR #12211: When TIMED=1, emit timing info for OCaml filesGaëtan Gilbert
2020-05-04nit: don't open Persistent_cache in micromegaGaëtan Gilbert
2020-05-04Merge PR #12220: [dune] [doc] TweaksGaëtan Gilbert
2020-05-04[dune] [doc] TweaksEmilio Jesus Gallego Arias
2020-05-04add order properties about boolOlivier Laurent
2020-05-04add incl_Forall_in_iffOlivier Laurent
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 22:27:53 +0000