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
Commit message (
Expand
)
Author
Age
*
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
*
|
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
*
|
Merge remote-tracking branch 'origin/pr/173' into trunk
Enrico Tassi
2016-06-14
|
\
\
*
|
|
Compilation via pack for plugins of the stdlib
Pierre Letouzey
2016-06-08
|
*
|
STM: proof block detection/error resilience API
Enrico Tassi
2016-06-06
|
/
/
*
|
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
*
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
*
Remove extraneous space in coqtop/pg output (bug #4675).
Guillaume Melquiond
2016-05-03
*
|
Moving the proof mode parsing management to Pcoq.
Pierre-Marie Pédrot
2016-03-19
*
|
Adding a universe argument to Pcoq.create_generic_entry.
Pierre-Marie Pédrot
2016-03-17
*
|
Removing the registering of default values for generic arguments.
Pierre-Marie Pédrot
2016-03-17
*
|
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-03-13
*
|
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: fix vernac classification.
Arnaud Spiwack
2015-03-31
*
Declarative mode: plug the specialised printers back.
Arnaud Spiwack
2015-03-31
*
Declarative mode: make it so that unfocussing can only be done for closed sub...
Arnaud Spiwack
2015-03-13
*
Declarative mode: remove dead code.
Arnaud Spiwack
2015-03-13
*
Declarative mode: remove a superfluous [set_proof_mode].
Arnaud Spiwack
2015-03-13
*
Declarative mode: fix the focus behaviour.
Arnaud Spiwack
2015-03-13
*
rewiring Czar printers that were disabled
Pierre Corbineau
2015-03-13
*
Fix double print in decl_mode.
Enrico Tassi
2015-03-11
*
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
[next]