index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
tacmach.ml
Commit message (
Expand
)
Author
Age
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Cleanup: removal of constr_of_global.
Matthieu Sozeau
2017-05-29
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
*
Merge branch 'master'.
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
*
|
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
*
|
Quote API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Proofview.Goal primitive now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Eqdecide API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Tacmach API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Goal API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Constr_matching 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
|
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
/
|
|
*
Fix #3441 Use pf_get_type_of to avoid blowup
Matthieu Sozeau
2016-11-04
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-05
|
\
|
|
*
Merge remote-tracking branch 'github/pr/263' into v8.6
Maxime Dénès
2016-10-03
|
|
\
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-27
|
\
|
|
|
*
|
Moving "move" in the new proof engine.
Hugo Herbelin
2016-09-24
|
|
*
Tracking careless uses of slow name lookup.
Pierre-Marie Pédrot
2016-09-09
|
|
/
*
|
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-30
*
|
CLEANUP: using |> operator more consistently
Matej Kosik
2016-08-30
*
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
/
*
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
Put the "cofix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "fix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "clear" tactic into the monad.
Pierre-Marie Pédrot
2016-05-16
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-17
|
\
*
|
CLEANUP: Renaming "Util.compose" function to "%"
Matej Kosik
2016-02-17
|
*
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
/
|
*
|
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-02-15
|
*
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
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
Proofview.Goal.sigma returns an indexed evarmap.
Pierre-Marie Pédrot
2015-10-20
*
|
Indexing Proofview.goals with a stage.
Pierre-Marie Pédrot
2015-10-20
|
/
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Update headers.
Maxime Dénès
2015-01-12
*
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
2015-01-08
*
Removing useless flag of the historical move tactic.
Pierre-Marie Pédrot
2014-11-22
*
Removing the legacy intro tactic code.
Pierre-Marie Pédrot
2014-11-07
[next]
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Gaetan Gilbert
Hugo Herbelin
Matej Kosik
Matej Kosik