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
*
Remove unused module definition after merging PR#592.
Maxime Dénès
2017-05-02
*
Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.
Maxime Dénès
2017-05-02
|
\
|
*
Fix bug #5501: Universe polymorphism breaks proof involving auto.
Pierre-Marie Pédrot
2017-04-30
*
|
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-27
|
/
*
[flags] Deprecate is_silent/is_verbose in favor of single flag.
Emilio Jesus Gallego Arias
2017-04-21
*
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
|
\
*
|
Quick hack to fix interpretation of patterns in Ltac.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing a subtle nf_enter in Class_tactics.
Pierre-Marie Pédrot
2017-02-14
*
|
Chasing a few unsafe constr coercions.
Pierre-Marie Pédrot
2017-02-14
*
|
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
|
Evar-normalizing functions now act on EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing compatibility layers related to printing.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
*
|
Removing some return type compatibility layers in Termops.
Pierre-Marie Pédrot
2017-02-14
*
|
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Eliminating parts of the right-hand side compatibility layer
Pierre-Marie Pédrot
2017-02-14
*
|
Hints API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Equality API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Clenv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Goal API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Pretyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Patternops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Typing API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-12-07
|
|
\
|
|
*
Fix bug #5232: proper globalization of hints paths
Matthieu Sozeau
2016-11-30
|
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
/
|
|
|
|
/
|
*
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
|
|
|
/
|
|
/
|
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
|
|
*
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
|
|
/
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-17
|
\
|
|
*
Using "simple apply" and "simple eapply" in the trace of auto.
Hugo Herbelin
2016-10-14
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-12
|
\
|
|
*
Fix bug #4958: [debug auto] should specify hint databases.
Pierre-Marie Pédrot
2016-10-12
*
|
Untangling Tacexpr from lower strata.
Pierre-Marie Pédrot
2016-09-15
*
|
Unplugging Pptactic from Ppvernac.
Pierre-Marie Pédrot
2016-09-08
*
|
Making Hints generic in the use of external tactics.
Pierre-Marie Pédrot
2016-09-08
*
|
Unplugging Tacexpr in several interface files.
Pierre-Marie Pédrot
2016-09-08
*
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
*
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
|
/
|
/
|
|
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
*
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
/
[next]