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
*
Efficient computation of the names contained in an environment.
Pierre-Marie Pédrot
2017-09-28
*
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
*
Merge PR #830: Moving assert (the "Cut" rule) to new proof engine
Maxime Dénès
2017-08-29
|
\
*
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
*
Moving "assert" (internally "Cut") to the new proof engine.
Hugo Herbelin
2017-06-25
|
/
*
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
[next]
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Matthieu Sozeau
Gaetan Gilbert
Matej Kosik
Matej Kosik