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
*
Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], as
msozeau
2009-09-03
*
Postpone checking of Local/Global to allow grammar extensions to use it
msozeau
2009-09-02
*
Stop unnecessary use of lazy values for constraints, simplifying
msozeau
2009-09-02
*
Hack to correctly get ill-formed rec body exceptions even
msozeau
2009-09-02
*
Fix notation for ~x in theories/Unicode/Utf8.v
glondu
2009-08-31
*
Fix minor spelling error
glondu
2009-08-29
*
update for why 2.19
marche
2009-08-28
*
Correction bug 2140.
soubiran
2009-08-27
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...
fbesson
2009-08-25
*
Delegate _all_ doc targets to stage2
lmamane
2009-08-25
*
install-doc* are PHONY
lmamane
2009-08-25
*
New tactic to rewrite decidability lemmas when one knows which side
herbelin
2009-08-24
*
A new kind of automatically generated scheme "congr" for equality types
herbelin
2009-08-23
*
Fix a small oversight in checker commit 12288.
herbelin
2009-08-23
*
Transfers to checker ("let"s in inductive arities + Coq root read-only).
herbelin
2009-08-22
*
new csdp cache + improved error message
fbesson
2009-08-20
*
new csdp cache + improved error message
fbesson
2009-08-20
*
adds a property on map
bertot
2009-08-19
*
adds lemmas on interactions between existsb, forallb, and app
bertot
2009-08-19
*
+ csdp.cache
fbesson
2009-08-15
*
Mise à jour du document de révision de la stdlib et déplacement de la
herbelin
2009-08-14
*
+Fix interface.
aspiwack
2009-08-14
*
Ajout de la gestion de Local et Global pour les options (au sens de
aspiwack
2009-08-14
*
Added profile.cmo in grammar.cma so that any functions in one of the
herbelin
2009-08-14
*
Tried to make F1 documentation tool working in CoqIDE.
herbelin
2009-08-14
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
Made unification patch 12268 even more ad hoc (if evars remain in a
herbelin
2009-08-13
*
Ensures that let-in's in arities of inductive types work well. Maybe not
herbelin
2009-08-11
*
Ajout des .annot dans le .gitignore.
aspiwack
2009-08-11
*
Fixed extra space in printing notation { x & P } + minor other things
herbelin
2009-08-11
*
Infix (r12268 continued)
herbelin
2009-08-11
*
Add support for "Infix ... := constr" instead of just "Infix ... := ref".
herbelin
2009-08-11
*
Relatively ad hoc fix to an ill-typed instantiation bug in type
herbelin
2009-08-11
*
Fixed incorrect optimization in Prettyp.pr_located_qualid introduced
herbelin
2009-08-07
*
Cleaning of Nametab continued + fixed a compilation bug in previous commit.
herbelin
2009-08-06
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Move out JMeq of subst for compatibility (it affects e.g. the
herbelin
2009-08-06
*
changed deprecated setoid into relation
amahboub
2009-08-05
*
- Add more precise error localisation when one of the application fails
herbelin
2009-08-04
*
Fixed subst failing when a truly heterogeneous JMeq hyp is in the
herbelin
2009-08-04
*
Added "etransitivity".
herbelin
2009-08-03
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Fixed a typo in "info" for tactic "right".
herbelin
2009-08-02
*
csdpcert + unix
fbesson
2009-08-01
*
addition of lia.cache - csdp.cache is now handled by micromega not csdpcert
fbesson
2009-07-31
*
micromega : Better parsing of formulae - smaller proof terms for Z - redesign...
fbesson
2009-07-30
*
psatz Z -> psatz Z 1
fbesson
2009-07-30
*
Git ignore files
herbelin
2009-07-30
*
For git users, a global .gitignore file
letouzey
2009-07-30
*
OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith
letouzey
2009-07-24
[next]