index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
extratactics.ml4
Age
Commit message (
Expand
)
Author
2018-01-08
Merge PR #6497: Add optimize_heap tactic for #6488
Maxime Dénès
2018-01-03
add optimize_heap tactic for #6488
Paul Steckler
2017-12-27
Remove the local polymorphic flag hack.
Maxime Dénès
2017-11-28
Merge PR #1033: Universe binder improvements
Maxime Dénès
2017-11-24
Use Evarutil.has_undefined_evars for tactic has_evar.
Gaëtan Gilbert
2017-11-24
Use Entries.constant_universes_entry more.
Gaëtan Gilbert
2017-11-24
Merge PR #6197: [plugin] Remove LocalityFixme über hack.
Maxime Dénès
2017-11-22
[plugin] Remove LocalityFixme über hack.
Emilio Jesus Gallego Arias
2017-11-19
Fix #5790: make Hint Resolve <- respect univ polymorphism flag.
Gaëtan Gilbert
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-10-26
Passing around the flag for injection so that tactics calling inj at
Hugo Herbelin
2017-09-28
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-08
Parse directly to Sorts.family when appropriate.
Gaëtan Gilbert
2017-09-04
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-08-01
Move type_uconstr to Tacinterp.
Maxime Dénès
2017-07-25
[api] Remove type equalities from API.
Emilio Jesus Gallego Arias
2017-07-17
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-15
plugins/ltac : avoid spurious .cmxs files
Pierre Letouzey
2017-06-13
Dualize the unsafe flag of refine into typecheck and make it mandatory.
Pierre-Marie Pédrot
2017-06-10
Remove (useless) aliases from the API.
Matej Košík
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-01
Merge PR#696: Trunk+cleanup constr of global
Maxime Dénès
2017-05-30
Support for using type information to infer more precise evar sources.
Hugo Herbelin
2017-05-29
Ltac cleanup: no more constr_of_global calls
Matthieu Sozeau
2017-05-29
Merge PR#512: [cleanup] Unify all calls to the error function.
Maxime Dénès
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
[coqlib] Move `Coqlib` to `library/`.
Emilio Jesus Gallego Arias
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-16
Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.
Hugo Herbelin
2017-05-11
Merge PR#201: Transparent abstract
Maxime Dénès
2017-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
Remove some unused values and types
Gaetan Gilbert
2017-04-25
Add transparent_abstract tactic
Jason Gross
2017-04-25
[location] [ast] Port module AST to CAst
Emilio Jesus Gallego Arias
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-24
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-07
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-04-06
Fix a normalization hotspot in computation of constr keys.
Pierre-Marie Pédrot
2017-04-01
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-23
Fast path for implicit tactic solving.
Pierre-Marie Pédrot
2017-02-17
Ltac as a plugin.
Pierre-Marie Pédrot
