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
*
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
*
Extension de l'utilisation de contradiction
herbelin
2003-10-19
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
Ground update + Linear removal
corbinea
2003-10-16
*
Branchement sur RIneq
herbelin
2003-10-16
*
Ground update changing left-arrow-arrow rule.
corbinea
2003-10-13
*
Ajout d'une fonction de recherche sur les composantes du nom des objets
herbelin
2003-10-13
*
Deplacement next_global_ident_away dans Termops
herbelin
2003-10-13
*
Ajout d'une fonction de recherche sur les composantes du nom des objets
herbelin
2003-10-13
*
Cablage en dur de inversion
herbelin
2003-10-10
*
show_subgoals dans Pfedit
herbelin
2003-10-10
*
Affichage des buts par Pfedit pour utilisation par les tactiques
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Compatibilite V7 des noms d'hypotheses
herbelin
2003-10-07
*
pour ocamlweb
letouzey
2003-10-06
*
distinguer interp_cs et interp_setcs
letouzey
2003-10-06
*
Cacher les .v8
herbelin
2003-10-03
*
Plus de nom commencant par '_' en V8
herbelin
2003-10-02
*
Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'
herbelin
2003-09-30
*
oups
letouzey
2003-09-28
*
2 pbs de plus réglés concernant Setoid Ring:
letouzey
2003-09-28
*
Un peu plus de souplesse dans la globalisation des noms utilises par les tact...
herbelin
2003-09-26
*
Utilisation de noms dans 'Implicit Arguments [...]'
herbelin
2003-09-23
*
Changement de l'afficheur pour que les variables liées aient un nom indépen...
herbelin
2003-09-23
*
Ajout fonctions syntaxe v8 pour contrib MapleMode
herbelin
2003-09-23
*
commit accidentel d'une bidouille
letouzey
2003-09-22
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
Système de renommage des noms de tactiques Ltac
herbelin
2003-09-22
*
suite (et fin) reparation Setoid Ring
letouzey
2003-09-22
[next]