index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
Suite commit 11236
notin
2008-07-24
*
A try at allowing matching on applications as a binary syntax node by default.
msozeau
2008-07-22
*
Extraction: better dependency computation (after optimisations)
letouzey
2008-07-20
*
Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...
notin
2008-07-18
*
Modification rapide du message d'erreur lorsqu'un _ ne peut être
herbelin
2008-07-18
*
ROmega : make it work even if no Require Import ZArith has been done
letouzey
2008-07-16
*
Micromega: doc + test-suite update
fbesson
2008-07-07
*
Fix bug #1899: no more strange notations for Qge and Qgt
letouzey
2008-07-04
*
Correct a bug in the coercion code where we did not go under constants
msozeau
2008-07-02
*
Improved robustness of micromega parser. Proof search of Micromega test-suite...
fbesson
2008-07-02
*
Various bug fixes in type classes and subtac:
msozeau
2008-07-01
*
Correction bug "parser" suite changement syntaxe
herbelin
2008-06-29
*
Enhanced discrimination nets implementation, which can now work with
msozeau
2008-06-27
*
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...
notin
2008-06-25
*
Micromega : bugs fixes - renaming of tactics - documentation
fbesson
2008-06-25
*
Rename obligations_tactic to obligation_tactic and fix bugs #1893.
msozeau
2008-06-22
*
Code cleanup in typeclasses, remove dead and duplicated code.
msozeau
2008-06-21
*
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2008-06-21
*
Various improvements in handling of evars in general and typing
msozeau
2008-06-21
*
Little fixes: print unbound variable in error message (patch by Samuel
msozeau
2008-06-19
*
Improvements in subtac:
msozeau
2008-06-18
*
Compatibility fixes (Add Setoid bug and accidental introduction of a
msozeau
2008-06-18
*
Cleanup in subtac_cases, preparing to use improvements on return predicate
msozeau
2008-06-17
*
Add possibility to match on defined hypotheses, using brackets to
msozeau
2008-06-16
*
Correction parser révélé par test-suite
herbelin
2008-06-12
*
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-10
*
Suppression de la dépendance de Micromega envers Coq.Reals.Reals. Corrige le...
notin
2008-06-10
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Fixes incorrect handling of existing existentials variables in
msozeau
2008-06-03
*
Minor bug correction in recdef
jforest
2008-06-02
*
Improvements on coqdoc by adding more information into .glob
msozeau
2008-05-30
*
- Fix bug #1858, Hint Unfold calling the wrong locate function.
msozeau
2008-05-23
*
Strategy commands are now exported
barras
2008-05-22
*
refined the conversion oracle
barras
2008-05-21
*
Corrections d'erreurs rapportées par Frédéric Besson sur le précédent
herbelin
2008-05-20
*
Intégration de micromega ("omicron" pour fourier et sa variante sur Z,
herbelin
2008-05-19
*
Various fixes:
msozeau
2008-05-15
*
- Fix bug related to indices of fixpoints.
msozeau
2008-05-13
*
debug et nouvelles commandes Dp_prelude et Dp_predefined
filliatr
2008-05-13
*
- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to
msozeau
2008-05-12
*
- Cleanup parsing of binders, reducing to a single production for all
msozeau
2008-05-11
*
Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]
herbelin
2008-05-09
*
Autre oubli de la révision 10904
herbelin
2008-05-08
*
export Extract_env.mono_environment in the mli
letouzey
2008-05-07
*
Postpone the search for the recursive argument index from the user given
msozeau
2008-05-06
*
Mise en place d'un algorithme d'inversion des contraintes de type lors
herbelin
2008-05-05
*
Clarification de l'ordre d'interprétation des variables dans ltac. En
herbelin
2008-05-01
*
Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la
herbelin
2008-04-29
*
Suppression de la partie ML de la contrib correctness. Les fichiers
herbelin
2008-04-29
*
menage dans funind + deplaceemnt de recdef dans funind
jforest
2008-04-28
[next]