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
*
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-10-29
|
\
|
*
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
|
/
*
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
|
/
[next]