index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernacentries.ml
Commit message (
Expand
)
Author
Age
*
Better error message for non-existent required libraries with a From prefix.
Pierre-Marie Pédrot
2015-05-13
*
STM: process_error_hook set in Vernac where fname is known (fix #4229)
Enrico Tassi
2015-05-12
*
Add a [Redirect] vernacular command
Clément Pit--Claudel
2015-05-04
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Make "Add LoadPath" behave accordingly to its documentation.
Guillaume Melquiond
2015-04-02
*
Display the proper error message when Require fails to find a library.
Guillaume Melquiond
2015-04-02
*
From X Require Y looks for X with absolute path, disregarding -R.
Pierre-Marie Pédrot
2015-04-01
*
Putting the From parameter of the Require command into the AST.
Pierre-Marie Pédrot
2015-03-27
*
Load: don't give anomaly on aborted proofs (Close: #3882)
Enrico Tassi
2015-03-23
*
Do not prepend a "Error:" header when the error is expected by the user.
Guillaume Melquiond
2015-03-05
*
Fixing OCaml 3.12 compilation.
Pierre-Marie Pédrot
2015-02-27
*
Fixing bug #3249.
Pierre-Marie Pédrot
2015-02-27
*
Univs: Fix Check calling the kernel to retype in the wrong environment.
Matthieu Sozeau
2015-02-24
*
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-14
*
Optimized Import/Export the same way as Require Import/Export was
Hugo Herbelin
2015-02-04
*
Prevent spurious warnings about Arguments.
Guillaume Melquiond
2015-01-29
*
Isolate a function for printing evar sets.
Hugo Herbelin
2015-01-24
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Update headers.
Maxime Dénès
2015-01-12
*
In Show Universes, print universes before normalization.
Matthieu Sozeau
2015-01-05
*
Proof using: do not clear letins (unless they use a cleared var)
Enrico Tassi
2014-12-29
*
Proof using: call "clear" to remove from sight the vars not selected
Enrico Tassi
2014-12-28
*
remove debug prints (leftover)
Enrico Tassi
2014-12-28
*
Better doc and a few fixes for Proof using.
Enrico Tassi
2014-12-19
*
Proof using: New vernacular to name sets of section variables
Enrico Tassi
2014-12-18
*
Arguments: warn only if no option is given (Close 3860)
Enrico Tassi
2014-12-17
*
Fixing CAMLP4 compilation.
Pierre-Marie Pédrot
2014-12-16
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Error messages of Searchxxx are coherent with goal selector.
Pierre Courtieu
2014-12-16
*
About now accepts hypothesis names and goal selector.
Pierre Courtieu
2014-12-15
*
Util.un_op -> Option.default
Pierre Boutillier
2014-12-14
*
Searchxxx now interpret patterns in goal environment if any.
Pierre Courtieu
2014-12-12
*
Searchxxx now search also the hypothesis and support goal selector.
Pierre Courtieu
2014-12-12
*
Reactivating option "Set Printing Existential Instances" for asking printing ...
Hugo Herbelin
2014-12-04
*
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-03
*
Add an [Info Level] option to print info traces automatically.
Arnaud Spiwack
2014-11-01
*
Add [Info] command.
Arnaud Spiwack
2014-11-01
*
Show_script called only if in coqtop mode
Enrico Tassi
2014-10-31
*
Fixes for PG (Close 3763, 3770)
Enrico Tassi
2014-10-27
*
Change reduction_of_red_expr to return an e_reduction_function returning
Matthieu Sozeau
2014-10-24
*
Goal printing made uniform: always done in STM (close 3585)
Enrico Tassi
2014-10-22
*
Continuing experimental printing of the signature of open evars in
Hugo Herbelin
2014-10-21
*
Experimental printing of the signature of open evars in Check.
Hugo Herbelin
2014-10-17
*
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
*
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-10-07
*
Notation: option to attach extra pretty printing rules to notations
Enrico Tassi
2014-09-29
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Rework typeclass resolution and control of backtracking.
Matthieu Sozeau
2014-09-15
[next]