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
*
Ajout de la gestion de Local et Global pour les options (au sens de
aspiwack
2009-08-14
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
Add support for "Infix ... := constr" instead of just "Infix ... := ref".
herbelin
2009-08-11
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
- Add more precise error localisation when one of the application fails
herbelin
2009-08-04
*
Added "etransitivity".
herbelin
2009-08-03
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Use user-given implicits from the arity in inductive definitions.
msozeau
2009-07-08
*
Jolification : tentative de supprimer les "( evd)" et associés qui
aspiwack
2009-07-07
*
Support for binding Coq root read-only in -R option
herbelin
2009-07-01
*
Use more consistent resolution parameters in Program and regular typing
msozeau
2009-06-18
*
Fix "unsatisfiable constraints" error messages to include all the
msozeau
2009-06-18
*
Correct typo: -noglob takes no argument.
msozeau
2009-06-13
*
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
[next]