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
...
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Misc improvements about evar_map
letouzey
2010-12-15
*
Add improved indenters that rely on the current proof state to choose the ind...
gmelquio
2010-12-14
*
First release of Vector library.
pboutill
2010-12-10
*
Fixing bug using explictly declared implicit arguments in inductive arities.
herbelin
2010-12-03
*
Redirect stdout to stderr in -ideslave
glondu
2010-12-03
*
Fixing a bug introduced in r12304 (move of interpretation of
herbelin
2010-12-02
*
Do not throw an error for anonymous generalized binders as they will be
msozeau
2010-11-18
*
Remove redundant clause (and fix compatibility issue)
glondu
2010-11-16
*
Minor fixes from Gregory Malecha. A typo fixed and a better (located)
msozeau
2010-11-15
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Add information of localisation when an error involving an "implicit
herbelin
2010-11-07
*
correcting a non catch error reported as an anomaly (Ploc.Exc)
jforest
2010-11-07
*
In Univ, unify order_request and constraint_type
glondu
2010-11-03
*
Output universe graph in DOT language if output file ends in .dot or .gv
glondu
2010-11-02
*
More generic Univ.dump_universes
glondu
2010-11-02
*
Move stuff about positive into a distinct PArith subdir
letouzey
2010-11-02
*
Restored checking that _all_ arguments of the command line are meaningful
herbelin
2010-11-01
*
Add tolerance for existential variables in Check.
herbelin
2010-10-31
*
Minor code improvements around libobject
herbelin
2010-10-31
*
Minor factorization of the part of the code used for Unnamed_thm saving.
herbelin
2010-10-31
*
Compatibility camlp4/camlp5
herbelin
2010-10-26
*
Fail, when successful, prints something only in verbose mode
glondu
2010-10-26
*
Fixing bug #2412, continued (preprocessing of Ltac Debug errors
herbelin
2010-10-23
*
Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431).
herbelin
2010-10-23
*
About "unsupported" unicode characters in notations.
herbelin
2010-10-17
*
Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping
herbelin
2010-10-11
*
Fix bug# 2392
msozeau
2010-10-07
*
Remove Explain* vernacs
glondu
2010-10-06
*
Remove VernacGo
glondu
2010-10-06
*
Two [Evd.fold] turned into [Evd.fold_undefined].
aspiwack
2010-10-04
*
Avoid raising an anomaly when an error encapsulated with a dummy
herbelin
2010-10-03
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Making display of various informations about constants more modular:
herbelin
2010-10-03
*
Fix bug #2321, allowing "_" named projections in classes. Not realizing
msozeau
2010-09-28
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Fix function applications without labels (OCaml warning 6)
glondu
2010-09-28
*
Fixed a bug in printing fix/cofix error messages when several
herbelin
2010-09-24
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 too
herbelin
2010-09-18
*
Fixing bugs #2347 (part 2) and #2388: error message printing was done
herbelin
2010-09-18
*
CoqIDE argv parsing delegated to coqtop
vgross
2010-09-14
*
Fix unescaped end-of-lines (OCaml warning 29)
glondu
2010-09-13
*
* removed declare_constant and declare_internal_constant
vsiles
2010-09-02
*
v13392 port from v8.3 to trunk : correct message when defining inductive schemes
vsiles
2010-09-02
*
* By default, load proof terms.
regisgia
2010-08-31
*
* scripts/Coqc toplevel/Usage:
regisgia
2010-08-27
*
* toplevel/Coqtop: Reactivate -dont-load-proofs option.
regisgia
2010-08-27
*
* lib/Flags: Replace dont_load_proofs by load_proofs since not loading
regisgia
2010-08-27
*
Fix an error message ot having the ERror: prefix.
courtieu
2010-08-26
[prev]
[next]