index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ...
Pierre-Marie Pédrot
2018-06-04
|
\
*
\
Merge PR #7640: Small refactoring to clarify make_local_hint_db.
Pierre-Marie Pédrot
2018-06-04
|
\
\
*
\
\
Merge PR #7649: Remove some dead code in class_tactics.ml
Pierre-Marie Pédrot
2018-06-04
|
\
\
\
*
\
\
\
Merge PR #7637: Fix an outdated comment refering to lib/dnet.mli
Pierre-Marie Pédrot
2018-06-03
|
\
\
\
\
|
|
|
|
*
Cleaning, documentation, uniformisation of the Coq extension of List.
Hugo Herbelin
2018-06-03
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Merge PR #7234: Reduce circular dependency constants <-> projections
Maxime Dénès
2018-06-01
|
\
\
\
\
|
|
|
*
|
Remove some dead code in class_tactics.ml
Armaël Guéneau
2018-05-31
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Merge PR #6969: [api] Remove functions deprecated in 8.8
Maxime Dénès
2018-05-31
|
\
\
\
\
|
|
*
|
|
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-05-31
*
|
|
|
|
Move interning the [hint_pattern] outside the Typeclasses hooks.
Gaëtan Gilbert
2018-05-30
|
|
/
/
/
|
/
|
|
|
|
*
|
|
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-30
|
/
/
/
*
|
|
Merge PR #7558: [api] Make `vernac/` self-contained.
Maxime Dénès
2018-05-30
|
\
\
\
|
|
|
*
Small refactoring to clarify make_local_hint_db.
Théo Zimmermann
2018-05-30
|
|
*
|
Fix an outdated comment refering to lib/dnet.mli
Armaël Guéneau
2018-05-30
|
|
|
/
*
|
/
Tactics.introduction: remove dangerous option ~check
Enrico Tassi
2018-05-28
|
|
/
|
/
|
|
*
[api] Make `vernac/` self-contained.
Emilio Jesus Gallego Arias
2018-05-27
|
*
[tactics] Turn boolean locality hint parameter into a named one.
Emilio Jesus Gallego Arias
2018-05-27
*
|
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-25
|
/
*
[tactics] Remove anonymous fix/cofix form.
Emilio Jesus Gallego Arias
2018-05-24
*
Moving Option.smart_map to Option.Smart.map.
Hugo Herbelin
2018-05-23
*
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
*
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-23
*
Split off Universes functions about substitutions and constraints
Gaëtan Gilbert
2018-05-17
*
Split off Universes functions dealing with generating new universes.
Gaëtan Gilbert
2018-05-17
*
Stop using Universes.subst(_opt)_univs_constr
Gaëtan Gilbert
2018-05-17
*
Deprecate Typing.e_* functions
Gaëtan Gilbert
2018-05-14
*
Deprecate Refiner [evar_map ref] exported functions.
Gaëtan Gilbert
2018-05-14
*
Deprecate Evarconv.e_conv,e_cumul
Gaëtan Gilbert
2018-05-11
*
Convert clear_hyps_in_evi to state passing style.
Gaëtan Gilbert
2018-05-11
*
Deprecate most evarutil evdref functions
Gaëtan Gilbert
2018-05-11
*
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.
Pierre-Marie Pédrot
2018-05-04
|
\
*
|
Make "intro"/"intros" progress on existential variables.
Hugo Herbelin
2018-05-02
*
|
[api] Move bullets and goals selectors to `proofs/`
Emilio Jesus Gallego Arias
2018-05-01
*
|
Merge PR #6935: Separate universe minimization and evar normalization functions
Pierre-Marie Pédrot
2018-04-30
|
\
\
*
|
|
Strict focusing using Default Goal Selector.
Gaëtan Gilbert
2018-04-29
*
|
|
tclSELECT: SelectAll never happens
Gaëtan Gilbert
2018-04-29
|
|
*
[api] Move `hint_info_expr` to `Typeclasses`.
Emilio Jesus Gallego Arias
2018-04-26
*
|
|
Improving error message for clear tactic (and indirect uses of it).
Hugo Herbelin
2018-04-24
|
|
/
|
/
|
|
*
Deprecate mixing univ minimization and evm normalization functions.
Gaëtan Gilbert
2018-04-17
|
/
*
Merge PR #7215: Deprecate the "simple subst" tactic.
Hugo Herbelin
2018-04-16
|
\
*
\
Merge PR #7200: [ltac] Deprecate nameless fix/cofix.
Maxime Dénès
2018-04-16
|
\
\
*
|
|
Evar maps contain econstrs.
Gaëtan Gilbert
2018-04-13
*
|
|
Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...
Pierre-Marie Pédrot
2018-04-13
|
\
\
\
|
|
*
|
[ltac] Deprecate nameless fix/cofix.
Emilio Jesus Gallego Arias
2018-04-13
|
|
/
/
|
/
|
|
|
|
*
Deprecate the "simple subst" tactic.
Pierre-Marie Pédrot
2018-04-10
|
|
/
|
/
|
*
|
[api] Move some types to their proper module.
Emilio Jesus Gallego Arias
2018-04-02
*
|
Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of tclTHEN...
Pierre-Marie Pédrot
2018-04-01
|
\
\
|
|
*
[econstr] Forbid calling `to_constr` in open terms.
Emilio Jesus Gallego Arias
2018-03-31
|
|
/
|
/
|
*
|
Fix #6631: Derive Plugin gives "Anomaly: more than one statement".
Pierre-Marie Pédrot
2018-03-29
[next]