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
*
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
*
Removing the old rename tactic.
Pierre-Marie Pédrot
2014-11-04
*
Change reduction_of_red_expr to return an e_reduction_function returning
Matthieu Sozeau
2014-10-24
*
Removing Convert_concl and Convert_hyp from Logic.
Hugo Herbelin
2014-10-09
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-05
*
Revert the two previous commits. I was testing in the wrong branch.
Pierre-Marie Pédrot
2014-09-04
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-04
*
Removing more tactic compatibility layer.
Pierre-Marie Pédrot
2014-08-01
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Rewriting [lapply] tactic in the new monad.
Pierre-Marie Pédrot
2014-04-27
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Removing tactic compatibility layer from Elim.
Pierre-Marie Pédrot
2014-04-22
*
Removing unused functions in Refiner.
Pierre-Marie Pédrot
2014-04-06
*
Removing tactic compatibility layer from Eqdecide.
Pierre-Marie Pédrot
2014-03-27
*
Removing Tacmach compatibility layer in Inv.
Pierre-Marie Pédrot
2014-03-26
*
Moving some tactic code to the new engine.
Pierre-Marie Pédrot
2014-03-26
*
Using non-normalized goals in tactic interpretation.
Pierre-Marie Pédrot
2014-03-19
*
Adding phantom types to discriminate normalized goals, and adding a way to
Pierre-Marie Pédrot
2014-03-19
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
Pierre Letouzey
2014-03-02
*
Algebraized "No such hypothesis" errors
Pierre-Marie Pédrot
2014-01-06
*
Made Proofview.Goal.hyps a named_context.
aspiwack
2013-11-02
*
Less use of the list-based interface for goal-bound tactics.
aspiwack
2013-11-02
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Merging Context and Sign.
ppedrot
2013-04-29
[next]