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