index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
decl_mode
/
decl_proof_instr.ml
Commit message (
Expand
)
Author
Age
*
Moving the Ltac plugin to a pack-based one.
Pierre-Marie Pédrot
2017-02-17
*
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
*
\
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-07
|
\
\
|
*
\
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-07
|
|
\
\
|
|
*
|
Fixing what is probably a typo in Strict Proofs mode (#5062).
Hugo Herbelin
2016-09-03
*
|
|
|
CLEANUP: using |> operator more consistently
Matej Kosik
2016-08-30
*
|
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
*
|
|
|
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
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
|
|
/
|
/
|
*
|
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
|
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
|
Removing the old refine tactic from the Tactics module.
Pierre-Marie Pédrot
2016-05-17
*
|
Put the "generalize" 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
*
|
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-02-22
*
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
*
|
|
Renaming functions in Typing to stick to the standard e_* scheme.
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
*
|
Constraining refine to monotonic functions.
Pierre-Marie Pédrot
2015-10-18
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
Removing uselessly duplicated function in Evd.
Pierre-Marie Pédrot
2015-09-27
|
/
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Declarative mode: remaining goals are "given up" when closing blocks.
Arnaud Spiwack
2015-04-22
*
Declarative mode: fix proof modes.
Arnaud Spiwack
2015-03-31
*
Declarative mode: remove a superfluous [set_proof_mode].
Arnaud Spiwack
2015-03-13
*
Declarative mode: fix the focus behaviour.
Arnaud Spiwack
2015-03-13
*
Removing the unused field ltacrecvars of tactic internalization.
Pierre-Marie Pédrot
2015-02-27
*
Update headers.
Maxime Dénès
2015-01-12
*
Writing rename_hyps in the new monad.
Pierre-Marie Pédrot
2014-11-03
*
Remove the deprecated open-constr based refine.
Arnaud Spiwack
2014-10-22
*
A version of convert_concl and convert_hyp in new proof engine.
Hugo Herbelin
2014-10-09
*
decl_mode: stay in declarative mode
Enrico Tassi
2014-10-06
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
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
*
Typing.sort_of does not leak evarmaps anymore.
Pierre-Marie Pédrot
2014-09-04
*
A reorganization of the "assert" tactics (hopefully uniform naming
Hugo Herbelin
2014-08-18
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
[next]