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
*
Sequent: generic equality on constr replaced by destructors
puech
2011-07-29
*
Sequent: generic equality on ident replaced by id_ord
puech
2011-07-29
*
Instances: generic equality on global_reference replaced by RefOrdered.compare
puech
2011-07-29
*
Unify: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Eqschemes: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Evarutil: generic equality on constr replaced by destructors
puech
2011-07-29
*
Heads: generic equality on constr replaced by destructor
puech
2011-07-29
*
Environ: generic equality on named_context replaced by named_context_equal
puech
2011-07-29
*
Evarconv: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Equality: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Cases: generic equality on constr replaced by destructors
puech
2011-07-29
*
Tactics: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Classops: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Class: generic equality on constr replaced by destructors
puech
2011-07-29
*
Evarutil: generic equality on constr replaced by eq_constr (x2)
puech
2011-07-29
*
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
[next]