index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
suppression du retour chariot a la fin de print_pure_constr
barras
2002-02-07
*
un assert false de trop (MLexn peut avoir des args)
letouzey
2002-02-07
*
oubli
letouzey
2002-02-06
*
gros changement dans mlutil.ml: ajout d'une elimination globale des prop
letouzey
2002-02-06
*
affichage des messages d'erreur pour Stack_overflow, Out_of_memory, Break
barras
2002-02-06
*
evaluable_constant retournait vrai pour les constantes opaques, ce qui faisait
barras
2002-02-05
*
exclusion des rertoires de test de l'extraction
letouzey
2002-02-05
*
Ajout d'optimisations locales kill_prop
letouzey
2002-02-05
*
exceptionmal ratrappee
barras
2002-02-04
*
maj newsyntax
barras
2002-02-04
*
Ajout tactiques Rename et Pose; modifications pour Inversion
herbelin
2002-02-01
*
adaptation de l'extraction aux changements de Christine concernant rec/rect e...
letouzey
2002-01-31
*
changement generation de schema d'elimination, False_rec est primitif, Constr...
mohring
2002-01-31
*
extraction des CoInductives via les Lazy d'ocaml
letouzey
2002-01-31
*
cosmetique
herbelin
2002-01-30
*
ajout list_split3, pr_semicolon et pr_bar
herbelin
2002-01-30
*
Reparation erreur de syntaxe
mohring
2002-01-30
*
modification de la definition des def inductives unitaires et autorisation d'...
mohring
2002-01-29
*
condition de positivite moins stricte vis-a-vis des parametres (cf bug de Edu...
barras
2002-01-29
*
Test affichage O de nat dans une expression sur Z
herbelin
2002-01-25
*
Bug affichage de O (de nat) dans une expression sur Z
herbelin
2002-01-25
*
*** empty log message ***
herbelin
2002-01-25
*
Zdiv et Zmod dans Zcomplements
filliatr
2002-01-25
*
patch Omega (bug 129)
filliatr
2002-01-25
*
Correction bug 'Check [b]if b then O else O'
herbelin
2002-01-25
*
Remplacement cut_intro par true_cut_anon pour Inversion
herbelin
2002-01-25
*
Bug calcul de la signature incorrecte en présence de letin
herbelin
2002-01-25
*
Correction de l'ordre des open (sachant que de toutes façons, un
herbelin
2002-01-24
*
Remplacement cut_intro par true_cut_anon
herbelin
2002-01-24
*
Bug calcul de la signature incorrecte en présence de letin
herbelin
2002-01-24
*
code mort
herbelin
2002-01-24
*
Cas LetIn superflu dans check_construct car normalisation préalable
herbelin
2002-01-24
*
Bug dépendances en les corps des let-in oubliées
herbelin
2002-01-24
*
Réparation bug 'known_dependent'
herbelin
2002-01-24
*
In Pcoq, the search commands had an erroneous behavior. Bound variables
bertot
2002-01-23
*
paquet Debian 7.2-3
courant
2002-01-23
*
mise a jour
filliatr
2002-01-21
*
warning en mode verbeux seulement
filliatr
2002-01-21
*
Correction de Pierre Crégut pour le bug MERGE_EQ
herbelin
2002-01-21
*
Ajout test de Pierre Crégut
herbelin
2002-01-21
*
Zinv -> Zopp
filliatr
2002-01-21
*
*** empty log message ***
herbelin
2002-01-18
*
*** empty log message ***
herbelin
2002-01-18
*
Bug MERGE_EQ
herbelin
2002-01-18
*
Bug commentaire (*i i*)
herbelin
2002-01-18
*
Pas d'assert false dans un try with !
herbelin
2002-01-18
*
amadouage de coqweb
letouzey
2002-01-18
*
Plusieurs arguments autorisés pour Require et Read Module
herbelin
2002-01-18
*
Plusieurs arguments autorisés pour Require et Read Module; mise en place d'u...
herbelin
2002-01-18
[next]