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
*
Retour des _eq en v8
herbelin
2003-11-27
*
Remplacement de l'indicateur de date "@" par 'at'
herbelin
2003-11-26
*
just forgot something in previous commit
corbinea
2003-11-26
*
removal of CC.v lemata in cc (deprecated)
corbinea
2003-11-26
*
Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...
herbelin
2003-11-25
*
CC: added injection theory
corbinea
2003-11-25
*
Prise en compte des defs syntaxiques dans is_global et global_reference qui p...
herbelin
2003-11-24
*
Code simplification in CC
corbinea
2003-11-20
*
Prise en compte renommages
herbelin
2003-11-19
*
correction suite ajout nouvelles tactiques
clrenard
2003-11-18
*
Ajout Print Implicit avec depliage du type
herbelin
2003-11-15
*
Ordre standard pour l'associativite
herbelin
2003-11-14
*
Correction chemin de Z
herbelin
2003-11-14
*
moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...
barras
2003-11-13
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Bug TacId
herbelin
2003-11-12
*
Restructuration ZArith
herbelin
2003-11-12
*
Noms/énoncés plus canoniques
herbelin
2003-11-12
*
petits changements de syntaxe
barras
2003-11-12
*
les modifs depuis la 7.4
letouzey
2003-11-12
*
TODO
letouzey
2003-11-12
*
Extraction Module M devient simplement Extraction M
letouzey
2003-11-12
*
Suppression SearchNamed finalement redondant avec SearchAbout
herbelin
2003-11-10
*
le pb du <<.v vu comme module>> engendre maintenant une erreur
letouzey
2003-11-10
*
message informant de l'ecriture d'un fichier extrait
letouzey
2003-11-10
*
révision du traitement des axiomes non réalisés
letouzey
2003-11-10
*
essai d'extraction sous un module
letouzey
2003-11-10
*
factorisation de (recursive) library
letouzey
2003-11-09
*
Traduction semantique des InHyp de clause en InHypValue si local def
herbelin
2003-11-09
*
Traduction semantique des InHyp de clause en InHypValue si local def
herbelin
2003-11-09
*
Added Instantiate ... in
corbinea
2003-11-06
*
Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...
herbelin
2003-11-05
*
Renommage canonique d'un lemme redondant
herbelin
2003-11-05
*
Déport des lemmes de Omega de ZArith vers OmegaLemmas
herbelin
2003-11-05
*
Renommage canonique d'un lemme redondant
herbelin
2003-11-05
*
Extension de zarith
herbelin
2003-11-04
*
Protection contre les buts sans inegalite
herbelin
2003-11-02
*
Ajout CPatNotation, PrintVisibility
herbelin
2003-11-01
*
Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...
herbelin
2003-11-01
*
Redirected some of the verbose jprover output through the Pp module.
corbinea
2003-10-30
*
Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...
herbelin
2003-10-30
*
traduction des noms de correctness
herbelin
2003-10-30
*
Ajout notations pour les expressions dans un anneau
herbelin
2003-10-28
*
Simplification preuve
herbelin
2003-10-28
*
Conjecture declare maintenant un axiome; reorganisation VernacDefinition
herbelin
2003-10-23
*
Jprover bugfix (hopefully !)
corbinea
2003-10-23
*
Ajout NArithRing
herbelin
2003-10-22
*
Integration de SearchNamed dans SearchAbout
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Construction des chemins de constantes plus robuste
herbelin
2003-10-21
[next]