aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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 ↵Hugo Herbelin
map_eq_app Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06[ci] bump elpi to 1.11Enrico Tassi
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06Merge PR #12018: Adding properties about implb in Bool.vAnton Trunov
Ack-by: Blaisorblade Reviewed-by: anton-trunov
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`. Fixes #12257 Fixes #12258
2020-05-06Fix #12211Jason Gross
I forgot to test #12211 sufficiently; it was emitting timing info without saying which file was being timed, because the evaluation of `$@` was performed at the definition of `OCAMLC`. This fixes that issue of 8bd559370f51d7cc1877380a5ad726da67ceb0fa by delaying the evaluation of the definitions of `OCAMLC` and `OCAMLOPT` to the running of the recipies.
2020-05-06Layout of Bool.v, especially for coqdoc.Hugo Herbelin
2020-05-06Adding properties about implb.Hugo Herbelin
This addresses a question on gitter (April 4).
2020-05-06Moving lazymatch and multimatch to simple identifiers.Hugo Herbelin
2020-05-06Stop keeping outdated static list of keywords.Hugo Herbelin
The real list is computed by tok_using in CLexer.
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
Incidentally removing "discriminated", "(bfs)" and "(dfs)" from keywords. It is enough to make them normal identifiers. Note: - keywords reserved by the tactics are: ** [= _eqn |- by using - keywords reserved by ltac are: lazymatch multimatch ||
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
Reviewed-by: gares
2020-05-05Merge PR #12252: [refman] Add missing (only parsing) to example of compat ↵Clément Pit-Claudel
notations.
2020-05-05Fix GeoCoq slowdown.Pierre-Marie Pédrot
There is no point in normalizing the goal in the legacy refiner because the function is actually insensitive to evars.
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
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2020-05-04update documentation for overlay buildingOlivier Laurent
2020-05-04Merge PR #12211: When TIMED=1, emit timing info for OCaml filesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-04nit: don't open Persistent_cache in micromegaGaëtan Gilbert
2020-05-04Merge PR #12220: [dune] [doc] TweaksGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-04[dune] [doc] TweaksEmilio Jesus Gallego Arias
Close #12167
2020-05-04add order properties about boolOlivier Laurent
2020-05-04add incl_Forall_in_iffOlivier Laurent
2020-05-04strenghten nth_extOlivier Laurent
2020-05-04add incl_map incl_filter NoDup_filterOlivier Laurent
2020-05-03Merge PR #12231: Simplify division of Cauchy realsMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-03Merge PR #12238: [stdlib] [CPermutation] patch for #12031Hugo Herbelin
Reviewed-by: herbelin
2020-05-03[declare] Add deprecation notices for compat modules.Emilio Jesus Gallego Arias
We will remove this modules and submit the overlays once the refactoring is done as to avoid churn.
2020-05-03[funind] Remove use of low-level entries in scheme generation.Emilio Jesus Gallego Arias
This is needed to make this low-level entry structures privates; moreover, the code seems much clearer using the higher-level API. Some more cleanup needs to be done but this is clearly a step forward IMHO.
2020-05-03[funind] Make `build_functional_principle` use a functional evar_mapEmilio Jesus Gallego Arias
2020-05-03Merge PR #12197: LtacProf now handles multi-success backtrackingPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-03Add tests uncovered during bug chasing in the CI.Pierre-Marie Pédrot
2020-05-03Add overlays.Pierre-Marie Pédrot
2020-05-03Further port of ssr tacticsPierre-Marie Pédrot
2020-05-03Further port of SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Remove legacy API in SSR.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tacticsPierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 10:12:35 +0000