index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Equality: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Tactics: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Tactics: generic equality on named_declaration replaced by eq_named_declaration
puech
2011-07-29
*
Term: added function eq_named_declaration
puech
2011-07-29
*
Evarutil: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Tacred: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Hipattern: two generic equalities on constr spotted & rewritten
puech
2011-07-29
*
Indtypes: remove useless and wrong generic equality test on constr array
puech
2011-07-29
*
Term: slight reorganization of the file
puech
2011-07-29
*
Term_typing, Typeops: replace some generic '=' on constr by eq_constr
puech
2011-07-29
*
Term: Refactoring of hashconsing
puech
2011-07-29
*
argument renaming in liftn (match with usual terminology)
puech
2011-07-29
*
Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)
letouzey
2011-07-28
*
Coqide: GEdit.combo is deprecated since Gtk2.4! We now use GEdit.combo_box_en...
pboutill
2011-07-27
*
Oversight in revision 14292.
pboutill
2011-07-27
*
Typo of bug 2577
pboutill
2011-07-27
*
or_introl is now too complicated for basic tests of test-suite/output/PrintIn...
pboutill
2011-07-26
*
Partial revert of r14292
pboutill
2011-07-26
*
ide/coq_lex.mll: restore the separate parsing of .. (fix #2578)
letouzey
2011-07-26
*
Integral domains
pottier
2011-07-26
*
Ring2 devient Ncring et la reification par les type classes est partagee
pottier
2011-07-26
*
All the parameters of Compare are implicits.
pboutill
2011-07-26
*
All the parameters of or can be implicits.
pboutill
2011-07-26
*
Same Implicit Arguments rule for sumbool and sumor.
pboutill
2011-07-26
*
Coqide: fixes and clarifications concerning sentence-terminators
letouzey
2011-07-25
*
Add a syntax entry for fully applied constructor pattern
pboutill
2011-07-22
*
Internalization of pattern carries a full intern_env
pboutill
2011-07-22
*
Allow custom targets without commands specified
pboutill
2011-07-22
*
For the beauty of tail recursion, a new list_addn
pboutill
2011-07-22
*
Fix typo in coqmktop help
glondu
2011-07-20
*
Fixed a "feature" of "inversion" and "dependent rewrite" revealed by
herbelin
2011-07-18
*
This adds two option tables 'Printing Record' and 'Printing Constructor'
herbelin
2011-07-16
*
This is exactly the structure needed to handle controlling printing
herbelin
2011-07-16
*
This option disables the use of the '{| field := ... |}' notation
herbelin
2011-07-16
*
Some facts about functional extensionality (especially alternative
herbelin
2011-07-16
*
More lemmas relating the different equivalent formulations of eq_dep.
herbelin
2011-07-16
*
Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)
herbelin
2011-07-16
*
Changed name of internally defined "_sym" scheme to avoid confusion with Logi...
herbelin
2011-07-16
*
Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...
herbelin
2011-07-16
*
Finally, pr_goal seems to work for printing v8.2 style goal in debugger.
herbelin
2011-07-16
*
Added a characterization of unique existence.
herbelin
2011-07-16
*
A correct error message for an unknown field in a record definition
pboutill
2011-07-15
*
Makefiles generated by coq_makefile can build %.cmx?a from %.mllib
pboutill
2011-07-11
*
Stores bullet stack on locally at the level of focuses rather than globally i...
aspiwack
2011-07-11
*
Coqide: undo comments (Second part of r14268)
pboutill
2011-07-08
*
coq_makefile logical path ending with '.' are correctly convert to physical path
pboutill
2011-07-07
*
coq_makefile bug fix 2405: cmxs are now made from cmx files
pboutill
2011-07-07
*
coq_makefile documentation in Refman and -h
pboutill
2011-07-07
*
coq_makefile doesn't complain anymore when a dir is both -I and -R
pboutill
2011-07-07
*
Bug 2217: In coqide, a comment alone is now a sentence that isn't send to coq
pboutill
2011-07-07
[next]