index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
Age
Commit message (
Expand
)
Author
2020-05-14
Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...
Hugo Herbelin
2020-05-14
Merge PR #11922: No more local reduction functions in Reductionops.
Maxime Dénès
2020-05-14
Tweak the error message of reference internalization.
Pierre-Marie Pédrot
2020-05-14
Generalize the interpretation of syntactic notation as reference to their head.
Pierre-Marie Pédrot
2020-05-14
Move the static check of evaluability in unfold tactic to runtime.
Pierre-Marie Pédrot
2020-05-14
Merge PR #12214: nit: don't open Persistent_cache in micromega
Vincent Laporte
2020-05-13
Merge PR #12229: Hopefully consensual cleaning of keywords
Théo Zimmermann
2020-05-13
Merge PR #12307: Cleaning up the legacy proof engine
Emilio Jesus Gallego Arias
2020-05-12
Merge PR #12223: Locating error again in atomic tactics (fixes #12152)
Pierre-Marie Pédrot
2020-05-12
Remove useless try-with clauses in newring.
Pierre-Marie Pédrot
2020-05-12
Remove useless try-with blocks in congruence.
Pierre-Marie Pédrot
2020-05-11
Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.
Hugo Herbelin
2020-05-11
Merge PR #12273: Deprecate Refiner API
Emilio Jesus Gallego Arias
2020-05-11
Merge PR #12129: Add a `with_strategy` tactic
Pierre-Marie Pédrot
2020-05-10
No more local reduction functions in Reductionops.
Pierre-Marie Pédrot
2020-05-10
Locating error again in TacAtom and TacAlias (fixes #12152, fixes #12255).
Hugo Herbelin
2020-05-09
Merge PR #12241: [declare] Merge DeclareDef into Declare
Gaëtan Gilbert
2020-05-09
Add a `with_strategy` tactic
Jason Gross
2020-05-09
Merge PR #12204: Ltac helper functions API
Hugo Herbelin
2020-05-09
Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...
Hugo Herbelin
2020-05-09
Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.
Maxime Dénès
2020-05-08
In non-strict mode, accept any variable as a tactic reference.
Pierre-Marie Pédrot
2020-05-08
Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpoints
Pierre-Marie Pédrot
2020-05-07
[declare] Merge DeclareDef into Declare
Emilio Jesus Gallego Arias
2020-05-07
Deprecate the legacy tacticals from module Refiner.
Pierre-Marie Pédrot
2020-05-07
Remove call to Refiner API from Funind.
Pierre-Marie Pédrot
2020-05-07
Port Evar_tactics to the new API.
Pierre-Marie Pédrot
2020-05-07
Merge PR #12236: [funind] Remove use of low-level entries in scheme generation.
Gaëtan Gilbert
2020-05-07
Export API to recover values out of Ltac application.
Pierre-Marie Pédrot
2020-05-07
Add helper API to define low-level Ltac functions.
Pierre-Marie Pédrot
2020-05-06
Moving lazymatch and multimatch to simple identifiers.
Hugo Herbelin
2020-05-06
Stop keeping outdated static list of keywords.
Hugo Herbelin
2020-05-06
Documenting plugin/tactic/stdlib keywords in corresponding chapters.
Hugo Herbelin
2020-05-05
Merge PR #12227: Spring cleaning of the tactic compatibility layer
Enrico Tassi
2020-05-05
[ssr] wrap a couple of exception with tclLIFT
Enrico Tassi
2020-05-04
[ssr] get rid of (pf_)mkSsrConst
Enrico Tassi
2020-05-04
nit: don't open Persistent_cache in micromega
Gaëtan Gilbert
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-03
[funind] Make `build_functional_principle` use a functional evar_map
Emilio Jesus Gallego Arias
2020-05-03
Further port of ssr tactics
Pierre-Marie Pédrot
2020-05-03
Further port of SSR tactics.
Pierre-Marie Pédrot
2020-05-03
Further port of the SSR tactics.
Pierre-Marie Pédrot
2020-05-03
Further port of the SSR tactics.
Pierre-Marie Pédrot
2020-05-03
Remove legacy API in SSR.
Pierre-Marie Pédrot
2020-05-03
Further port of the SSR tactics
Pierre-Marie Pédrot
2020-05-03
Further port of the SSR tactics.
Pierre-Marie Pédrot
2020-05-03
Further port of the SSR tactics.
Pierre-Marie Pédrot
2020-05-03
Further port of the SSR tactics.
Pierre-Marie Pédrot
2020-05-03
Further port of the SSR tactics.
Pierre-Marie Pédrot
[next]
