index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
Age
Commit message (
Expand
)
Author
2014-11-08
Continuing 3741c46fe134 on reporting ltac error.
Hugo Herbelin
2014-11-03
Now that evars can be parsed, protect strongly Check from calling kernel with...
Hugo Herbelin
2014-11-03
Show: do print the goals
Enrico Tassi
2014-11-01
Add an [Info Level] option to print info traces automatically.
Arnaud Spiwack
2014-11-01
Add [Info] command.
Arnaud Spiwack
2014-10-31
STM: new worker for queries
Enrico Tassi
2014-10-31
Show_script called only if in coqtop mode
Enrico Tassi
2014-10-27
Fixes for PG (Close 3763, 3770)
Enrico Tassi
2014-10-25
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-24
Change reduction_of_red_expr to return an e_reduction_function returning
Matthieu Sozeau
2014-10-23
Evd.future_goals: forgot to revert the list in two places.
Arnaud Spiwack
2014-10-22
Make rint_location_in_file resilient to Cd (close 3630)
Enrico Tassi
2014-10-22
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-21
Continuing experimental printing of the signature of open evars in
Hugo Herbelin
2014-10-17
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-14
Fix ML paths (thanks Jean-Marc Notin for bisecting it)
Enrico Tassi
2014-10-13
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-11
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-10
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-07
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-10-03
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-02
Implement module subtyping for polymorphic constants (errors on
Matthieu Sozeau
2014-10-02
Print type and environment of unsolved holes.
Arnaud Spiwack
2014-10-01
Fixing nice printing of error reporting with ml tactics bound to ltac names.
Hugo Herbelin
2014-09-30
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-29
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-27
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-19
Fixing bug #3646.
Pierre-Marie Pédrot
2014-09-18
mltop: when a plugin is loaded store its full path in the summary
Enrico Tassi
2014-09-17
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-16
Undo prints only if coqtop || emacs
Enrico Tassi
2014-09-16
better error message
Enrico Tassi
2014-09-15
Rework typeclass resolution and control of backtracking.
Matthieu Sozeau
2014-09-13
Providing a -type-in-type option for collapsing the universe hierarchy.
Hugo Herbelin
2014-09-12
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
[next]
