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
*
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
*
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
[next]