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
...
*
Use a lazy value for the message in FailError, so that it won't be
msozeau
2009-06-11
*
Fix implicit args code so that declarations are added for all
msozeau
2009-05-27
*
Stop using a "Manual Implicit Arguments" flag and support them as soon
msozeau
2009-05-27
*
Minor fixes in typeclasses:
msozeau
2009-05-16
*
Fix to my last notation patch: now fixpoint are correctly handled
vsiles
2009-05-13
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
Fix a small notation/scope bug:
vsiles
2009-04-30
*
- Fixed a little bug in previous commit (bad failure in case of unknown entry).
herbelin
2009-04-27
*
- Cleaning (unification of ML names, removal of obsolete code,
herbelin
2009-04-27
*
- Fixing #2090 (occur check missing when trying to solve evar-evar equation).
herbelin
2009-04-25
*
Backporting 12080 (fixing bug #2091 on bad rollback in the "where"
herbelin
2009-04-24
*
Fix bug #2089: correctly dealing with parameters and real arguments in
msozeau
2009-04-16
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
- Fixing bug #2084 (unification not checking sort constraints), hoping
herbelin
2009-04-08
*
- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing
herbelin
2009-04-08
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
Remove unused mli files
letouzey
2009-03-27
*
Backport from v8.2 branch of 11986 (interpretation of quantified
herbelin
2009-03-22
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20
*
- configure: affiche si le natdynlink est positionne
barras
2009-03-17
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
*
Better mechanism for loading initial plugins
letouzey
2009-03-14
*
Optionally list opaque constants in addition to axions/variables in
msozeau
2009-03-09
*
Timeout message was not always displayed
barras
2009-03-04
*
commande Timeout + compaction des traces de debug_tactic
barras
2009-03-04
*
Backtrack sur la mémoïsation de nf_evar.
aspiwack
2009-03-04
*
=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...
aspiwack
2009-02-27
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
Fix de divers petits problèmes d'installation
notin
2009-02-11
*
Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin
2009-02-11
*
Allow to turn contrib/subtac into a (nat)dynlink'able plugin
letouzey
2009-02-03
*
Revert changes in pcoq functions to restore compatibility with contribs
puech
2009-01-26
*
Petit nettoyage faisant suite au commit #11847 .
aspiwack
2009-01-23
*
Les records déclarés avec Record ne peuvent plus être récursifs (le
aspiwack
2009-01-19
*
- Structuring Numbers and fixing Setoid in stdlib's doc.
herbelin
2009-01-19
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
*
Getting rid of the previous implementation of setoid_rewrite which was
msozeau
2009-01-18
*
Last changes in type class syntax:
msozeau
2009-01-18
*
DISCLAIMER
puech
2009-01-17
*
Fixing #1960 (xml bug with external on goal variable) and #1961
herbelin
2009-01-14
*
Fixing/improving management of uniform prefix Local and Global
herbelin
2009-01-14
*
- Standardized prefix use of "Local"/"Global" modifiers as decided in
herbelin
2009-01-13
*
- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).
herbelin
2009-01-11
*
Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...
notin
2009-01-06
*
Completed 11745 (move of jprover to user contribs) and cleaned 11743
herbelin
2009-01-05
*
Bug dans commit 11743
herbelin
2009-01-04
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
Made the debugger work again:
herbelin
2009-01-02
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
[prev]
[next]