index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
hints.ml
Commit message (
Expand
)
Author
Age
*
Merge remote-tracking branch 'github/pr/339' into v8.6
Maxime Dénès
2016-11-07
|
\
|
*
Fixes to compile with ocaml 4.01
Matthieu Sozeau
2016-11-07
*
|
Merge remote-tracking branch 'github/pr/336' into v8.6
Maxime Dénès
2016-11-04
|
\
\
|
|
*
Lets Hints/Instances take an optional pattern
Matthieu Sozeau
2016-11-03
|
|
/
|
/
|
|
*
Remove v62 from the codebase.
Théo Zimmermann
2016-10-25
*
|
sections/hints: prevent Not_found in get_type_of
Matthieu Sozeau
2016-10-21
|
/
*
Using "simple apply" and "simple eapply" in the trace of auto.
Hugo Herbelin
2016-10-14
*
Fix bug #4958: [debug auto] should specify hint databases.
Pierre-Marie Pédrot
2016-10-12
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-27
|
\
*
|
Extend Hint Mode to handle the no-head-evar case
Matthieu Sozeau
2016-06-16
*
|
Revise syntax of Hint Cut
Matthieu Sozeau
2016-06-16
|
*
Univs/(e)auto: fix bug #4450 polymorphic exact hints
Matthieu Sozeau
2016-06-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
|
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
*
Hints/Univs: fix bug #4628 anomalies
Matthieu Sozeau
2016-05-23
*
|
Relying on generic arguments to represent Extern hints.
Pierre-Marie Pédrot
2016-03-20
*
|
Making Evarutil independent from Reductionops.
Pierre-Marie Pédrot
2016-03-20
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.
Pierre-Marie Pédrot
2015-12-28
|
/
*
Fix bug #4433, removing hack on evars appearing in a pattern from a
Matthieu Sozeau
2015-11-19
*
Hint Cut documentation and cleanup of printing (was duplicated and
Matthieu Sozeau
2015-11-04
*
Fixing a loop in checking hints with holes.
Hugo Herbelin
2015-10-24
*
Merge hint lists instead of appending them. (Fix bug #3199)
Guillaume Melquiond
2015-10-16
*
Exporting the original unprocessed hint in the hint running function.
Pierre-Marie Pédrot
2015-10-14
*
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
*
Fix bug #4354: interpret hints in the right env and sigma.
Matthieu Sozeau
2015-10-06
*
Univs: fix evar_map handling in Hint processing.
Matthieu Sozeau
2015-10-02
*
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Adding an option Loose Hint Behavior to handle hints loaded but not imported.
Pierre-Marie Pédrot
2015-05-12
*
Adding unique identifiers to hints.
Pierre-Marie Pédrot
2015-05-12
*
Rationalizing a bit the interface of Hints.
Pierre-Marie Pédrot
2015-05-11
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Ensuring purity of datastructures in the API.
Pierre-Marie Pédrot
2015-04-16
*
Cleaning up the implementation of search entries in Hints.
Pierre-Marie Pédrot
2015-04-14
*
Opaque implementation of auto tactics.
Pierre-Marie Pédrot
2015-04-14
*
More documented representation of hint objects.
Pierre-Marie Pédrot
2015-04-13
*
Fix bug #3590, keeping evars that are not turned into named metas by
Matthieu Sozeau
2015-03-03
*
Update headers.
Maxime Dénès
2015-01-12
*
Removing the last Evd.diff from Hints.
Pierre-Marie Pédrot
2014-10-27
*
Forgotten hints.ml{,i} files in 38b34dfffcc.
Hugo Herbelin
2014-10-08