index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
auto.ml
Commit message (
Expand
)
Author
Age
...
|
*
Fix bug #4537: Coq 8.5 is slower in typeclass resolution.
Pierre-Marie Pédrot
2016-01-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
merge
Matej Kosik
2016-01-11
|
\
\
|
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
|
Remove duplicate definition.
Guillaume Melquiond
2016-01-02
|
/
/
*
|
Removing the evar_map argument from s_enter.
Pierre-Marie Pédrot
2015-10-29
*
|
Proofview.Goal.sigma returns an indexed evarmap.
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
*
|
Removing tclEVARS in various places.
Pierre-Marie Pédrot
2015-10-19
|
*
Generalize fix for auto from PMP to eauto and typeclasses eauto.
Matthieu Sozeau
2015-10-16
|
/
*
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 bug #4354: interpret hints in the right env and sigma.
Matthieu Sozeau
2015-10-06
*
Rationalizing a bit the interface of Hints.
Pierre-Marie Pédrot
2015-05-11
*
Using tclZEROMSG instead of tclZERO in several places.
Pierre-Marie Pédrot
2015-04-23
*
Opaque implementation of auto tactics.
Pierre-Marie Pédrot
2015-04-14
*
Update headers.
Maxime Dénès
2015-01-12
*
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
2015-01-08
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Follow up to experimental eager evar unification in bcba6d1bc9:
Hugo Herbelin
2014-11-08
*
Proofview: split [V82] module into [Unsafe] and [V82].
Arnaud Spiwack
2014-10-22
*
Remaining tactics of the Auto module were put in the monad.
Pierre-Marie Pédrot
2014-10-15
*
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-10-07
*
Made Tacsubst independent of Auto at linking time so that Tacenv does
Hugo Herbelin
2014-10-01
*
Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.
Matthieu Sozeau
2014-09-27
*
Make pattern_of_constr typed so that we can infer the proper patterns
Matthieu Sozeau
2014-09-27
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Fix bug #3593, making constr_eq and progress work up to
Matthieu Sozeau
2014-09-17
*
Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
Matthieu Sozeau
2014-09-15
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
A step towards better differentiating when w_unify is used for subterm
Hugo Herbelin
2014-09-10
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible
Matthieu Sozeau
2014-08-25
*
Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it
Pierre-Marie Pédrot
2014-06-24
*
Less goal-entering.
Pierre-Marie Pédrot
2014-06-22
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Improve hotspot in Auto.
Pierre-Marie Pédrot
2014-06-17
*
Passing some tactics to the new monad type.
Pierre-Marie Pédrot
2014-06-12
*
Collecting in Namegen those conventional default names that are used in diffe...
Hugo Herbelin
2014-06-04
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fixing various backtrace recordings.
Pierre-Marie Pédrot
2014-04-25
*
Tentative fix for a very strange pervasive equality in Auto.
Pierre-Marie Pédrot
2014-03-07
*
Fixing generic equality in Auto.
Pierre-Marie Pédrot
2014-03-07
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
[prev]
[next]