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
*
Removed many calls to OCaml generic equality. This was done by
ppedrot
2012-10-29
*
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-10-26
*
Text inserted by insert_this_phrase_on_success correct tagging
pboutill
2012-10-23
*
Fix test-suite output/* in bench
pboutill
2012-10-17
*
univ inconsistency error message gives evidence of a cycle
barras
2012-10-17
*
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
letouzey
2012-10-16
*
When loading a plugin, prefer .cma to .cmo
gareuselesinge
2012-10-14
*
Turn mltop.ml4 into a regular ocaml file
letouzey
2012-10-06
*
still some more dead code removal
letouzey
2012-10-06
*
remove useless hidden_flag in TacMutual(Co)Fix
letouzey
2012-10-06
*
Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box
letouzey
2012-10-06
*
coqtop -time : display per-command timings
letouzey
2012-10-05
*
Improving error message when abtraction over goal (abstract_list_all
herbelin
2012-10-04
*
Adding a nominal typing layer to Metasyntax in order to clarify
ppedrot
2012-10-04
*
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-10-04
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Fixing #2865.
ppedrot
2012-09-25
*
More cleaning in CArray...
ppedrot
2012-09-18
*
Cleaning interface of Util.
ppedrot
2012-09-18
*
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-17
*
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-15
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Made Pp.std_ppcmds opaque.
ppedrot
2012-09-13
*
Fixed #2893.
ppedrot
2012-09-10
*
When asked for a SearchAbout request, Coq now returns a more precise
ppedrot
2012-09-09
*
Avoid [Loading ML file ...] messages when launching coqtop
letouzey
2012-09-07
*
Fix computation of obligations for mutually recursive definitions.
msozeau
2012-09-06
*
Rationalized the behaviour of "Next Obligation" and "Admit Obligations"
ppedrot
2012-09-05
*
Use fully-qualified Coq.Init.Prelude when starting coqtop
letouzey
2012-08-24
*
Assumption commands are now displayed as unsafe in Coqide.
aspiwack
2012-08-24
*
No more states/initial.coq, instead coqtop now requires Prelude.vo
letouzey
2012-08-23
*
Do not forget to build the unicode libraries, necessary to compile and launch...
msozeau
2012-08-22
*
Added support for option Local (at module level) in Tactic Notation.
herbelin
2012-08-11
*
Updating headers.
herbelin
2012-08-08
*
Vecnacentries.dump_global silently ignores exceptions
pboutill
2012-08-06
*
Dump references in reduction tactics
pboutill
2012-08-05
*
Dump references in Reset
pboutill
2012-08-05
*
Fixing test-suite
pboutill
2012-07-20
*
Let coqtop be a little more stupid in hint answer: otherwise, that
ppedrot
2012-07-20
*
Various minor fixes to coqdoc from A. Chlipala.
msozeau
2012-07-18
*
A new status Unsafe in Interface. Meant for commands such as Admitted.
aspiwack
2012-07-12
*
Ensure that a plugin init function is called only once
letouzey
2012-07-12
*
Vernacentries: minor code cleanup
letouzey
2012-07-12
*
Bug 2838: ExplApp in mutual inductive parameters
pboutill
2012-07-12
*
Set/Unset Atomic Load : a pragmatic solution for part 2 of #2820
letouzey
2012-07-11
*
Also allow Reset in Load'ed files
letouzey
2012-07-11
[next]