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
*
[proof] Deprecate redundant wrappers.
Emilio Jesus Gallego Arias
2017-06-11
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
Merge PR#608: Allow Ltac2 as a plugin
Maxime Dénès
2017-05-25
|
\
*
\
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-25
|
\
\
*
\
\
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
\
|
|
*
|
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-05-24
|
|
/
/
|
|
*
Allowing to pass arbitrary data in internalization environments.
Pierre-Marie Pédrot
2017-05-03
|
|
/
|
*
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
|
|
/
*
/
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
|
/
*
[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
[next]