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 branch 'v8.5'
Pierre-Marie Pédrot
2015-10-26
|
\
|
*
Fixing a loop in checking hints with holes.
Hugo Herbelin
2015-10-24
|
*
Backtracking on interpreting toplevel calls to exact in scope determined
Hugo Herbelin
2015-10-24
*
|
Proofview.Goal.sigma returns an indexed evarmap.
Pierre-Marie Pédrot
2015-10-20
*
|
Indexing Proofview.goals with a stage.
Pierre-Marie Pédrot
2015-10-20
*
|
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
*
|
Renaming Goal.enter field into s_enter.
Pierre-Marie Pédrot
2015-10-20
*
|
Expliciting the uses of the old Tacmach API in Tactics.
Pierre-Marie Pédrot
2015-10-19
*
|
Removing some unsafe uses of monotonicity.
Pierre-Marie Pédrot
2015-10-19
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
*
|
Type delayed_open_constr is now monotonic.
Pierre-Marie Pédrot
2015-10-19
|
*
Categorizing debug messages as such + NonLogical uses loggers.
Pierre Courtieu
2015-10-19
*
|
More monotonicity in Tactics.
Pierre-Marie Pédrot
2015-10-19
|
*
Turning anomaly into error for #4372 (weakness of inversion in the
Hugo Herbelin
2015-10-19
*
|
Removing tclEVARS in various places.
Pierre-Marie Pédrot
2015-10-19
*
|
Reducing the uses of tclEVARS in Tactics by using monotonous functions.
Pierre-Marie Pédrot
2015-10-19
*
|
Making Evarutil.new_evar monotonous.
Pierre-Marie Pédrot
2015-10-18
*
|
Constraining refine to monotonic functions.
Pierre-Marie Pédrot
2015-10-18
*
|
Clarifying and documenting the UState API.
Pierre-Marie Pédrot
2015-10-17
|
*
Generalize fix for auto from PMP to eauto and typeclasses eauto.
Matthieu Sozeau
2015-10-16
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-10-16
|
\
|
|
*
Merge hint lists instead of appending them. (Fix bug #3199)
Guillaume Melquiond
2015-10-16
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Fixing perfomance issue of auto hints induced by universes.
Pierre-Marie Pédrot
2015-10-14
|
*
Exporting the original unprocessed hint in the hint running function.
Pierre-Marie Pédrot
2015-10-14
|
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-12
|
\
|
|
*
Remove code that was already commented out.
Maxime Dénès
2015-10-12
|
*
Fixing bug #4366: Conversion tactics recheck uselessly convertibility.
Pierre-Marie Pédrot
2015-10-11
|
*
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Hugo Herbelin
2015-10-11
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-10
|
\
|
|
*
Refine fix for handling of the universe contexts of hints, depending on
Matthieu Sozeau
2015-10-09
|
*
Fix CFGV contrib: handling of global hints introducing global universes.
Matthieu Sozeau
2015-10-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
|
\
|
|
*
Fix bug #4354: interpret hints in the right env and sigma.
Matthieu Sozeau
2015-10-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
*
Univs: refined handling of assumptions
Matthieu Sozeau
2015-10-02
|
*
Univs: fix evar_map handling in Hint processing.
Matthieu Sozeau
2015-10-02
|
*
discriminate: Do fresh_global in the right env in presence of side-effects.
Matthieu Sozeau
2015-10-02
|
*
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
*
|
Removing uselessly duplicated function in Evd.
Pierre-Marie Pédrot
2015-09-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-25
|
\
|
|
*
Hopefully better names to constructors of internal_flag, as discussed
Hugo Herbelin
2015-09-23
|
*
Give a way to control if the decidable-equality schemes are built like
Hugo Herbelin
2015-09-23
|
*
Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.
Pierre-Marie Pédrot
2015-09-22
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-09-17
|
\
|
|
*
In pat/constr introduction patterns, fixing in a better way clearing problems
Hugo Herbelin
2015-09-16
|
*
Continuing investigation on how to preserve the locality of the action
Hugo Herbelin
2015-09-16
|
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Hugo Herbelin
2015-09-09
|
\
|
[next]