index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
...
*
Goal printing made uniform: always done in STM (close 3585)
Enrico Tassi
2014-10-22
*
Split [Proofview] into a file where the basic operations on the state are def...
Arnaud Spiwack
2014-10-22
*
Proofview: move more functions to the Unsafe module.
Arnaud Spiwack
2014-10-22
*
Remove the deprecated open-constr based refine.
Arnaud Spiwack
2014-10-22
*
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.
Arnaud Spiwack
2014-10-22
*
Continuing experimental printing of the signature of open evars in
Hugo Herbelin
2014-10-21
*
Now printing "now a keyword" only in verbose mode.
Hugo Herbelin
2014-10-17
*
Experimental printing of the signature of open evars in Check.
Hugo Herbelin
2014-10-17
*
Fix ML paths (thanks Jean-Marc Notin for bisecting it)
Enrico Tassi
2014-10-14
*
Fix typo, thanks Mike Shulman for spotting it
Enrico Tassi
2014-10-13
*
Emit a warning for void Arguments statement (Close 3713)
Enrico Tassi
2014-10-13
*
STM: primitives to snapshot a .vi while in interactive mode
Enrico Tassi
2014-10-13
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Coqinit: look in toploop/ even if configured with -local
Enrico Tassi
2014-10-13
*
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-11
*
Give the same argument name for the record binder of type class
Matthieu Sozeau
2014-10-10
*
Add debug printers for projections, fix printing of evar constraints
Matthieu Sozeau
2014-10-10
*
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-10-07
*
Fixing #3193 (honoring implicit arguments in local definitions).
Hugo Herbelin
2014-10-03
*
Fixing #3634 (wrong env in "cannot instantiate because not in its
Hugo Herbelin
2014-10-03
*
Implement module subtyping for polymorphic constants (errors on
Matthieu Sozeau
2014-10-02
*
Print type and environment of unsolved holes.
Arnaud Spiwack
2014-10-02
*
Fixing nice printing of error reporting with ml tactics bound to ltac names.
Hugo Herbelin
2014-10-01
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Notation: option to attach extra pretty printing rules to notations
Enrico Tassi
2014-09-29
*
do not explode if a plugin is not up to date on -help (Close: 3673)
Enrico Tassi
2014-09-29
*
Merging some functions from evarutil.ml/evd.ml.
Hugo Herbelin
2014-09-29
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Fixing bug #3646.
Pierre-Marie Pédrot
2014-09-19
*
mltop: when a plugin is loaded store its full path in the summary
Enrico Tassi
2014-09-18
*
Be more conservative and keep the use of eq_constr in pretyping/ functions.
Matthieu Sozeau
2014-09-17
*
Fix bug #3593, making constr_eq and progress work up to
Matthieu Sozeau
2014-09-17
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Undo prints only if coqtop || emacs
Enrico Tassi
2014-09-16
*
better error message
Enrico Tassi
2014-09-16
*
Rework typeclass resolution and control of backtracking.
Matthieu Sozeau
2014-09-15
*
Providing a -type-in-type option for collapsing the universe hierarchy.
Hugo Herbelin
2014-09-13
*
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
*
Add a flag for restricting resolution of typeclasses to
Matthieu Sozeau
2014-09-11
*
Fix categorization of recursive inductives.
Matthieu Sozeau
2014-09-10
*
Fixing localisation of tactic errors (my mistake in himsg.ml essentially).
Hugo Herbelin
2014-09-10
*
VernacExtend does not dispatch on type anymore.
Pierre-Marie Pédrot
2014-09-10
*
Load Prelude.vi if not Prelude.vo is found (Close: 3595)
Enrico Tassi
2014-09-09
*
Undo: if the ui is coqtop (command line) then Undo is not part of the doc.
Enrico Tassi
2014-09-09
*
toploop plugins taken into account when printing --help (close: 3535)
Enrico Tassi
2014-09-09
*
Removing dead code relative to the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Parsing of Type@{max(i,j)}.
Matthieu Sozeau
2014-09-08
*
Fixing bug #3492.
Pierre-Marie Pédrot
2014-09-07
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
[prev]
[next]