index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
...
*
bug #780: compilation of several units in the same coqtop process
barras
2004-07-13
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
MAJ numéro magique
herbelin
2004-04-14
*
Export de l'information si un inductive est un record ou non (pour xml)
herbelin
2004-03-31
*
The XML exportation hook for require is now active for:
sacerdot
2004-03-30
*
Distinction entre declarations internes (p.ex. _subproof) et declarations uti...
herbelin
2004-03-30
*
Crocret xml pour Require
herbelin
2004-03-29
*
Crochets pour exported les sections en xml
herbelin
2004-03-27
*
Memorisation du type de variable (Hyp or Var)
herbelin
2004-03-26
*
preparation packages V8.0-cdrom
barras
2004-03-15
*
Bug de Require multiple
herbelin
2004-01-28
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Changement numero magique; message d'erreur en cas de mauvaise syntaxe
herbelin
2003-12-23
*
Reset Initial uniquement interactivement
herbelin
2003-12-19
*
name_app accessible a tous dans Nameops
herbelin
2003-12-19
*
Options -strongly-constructive et -strongly-classical
herbelin
2003-10-28
*
Conjecture declare maintenant un axiome; reorganisation VernacDefinition
herbelin
2003-10-23
*
Deplacement de iter_constr_with_full_binders dans Termops
herbelin
2003-10-22
*
Nouvelle fonction cherchant tous les noms d'un suffixe donne
herbelin
2003-10-21
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
Mise en place d'un mecanisme ne chargeant pas les preuves opaques
herbelin
2003-10-08
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Fonctions utiles
herbelin
2003-09-23
*
Utilisation de noms dans 'Implicit Arguments [...]'
herbelin
2003-09-23
*
Mise en place d'implicites par noms en v8
herbelin
2003-09-21
*
Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...
herbelin
2003-09-12
*
Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...
herbelin
2003-09-12
*
Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...
herbelin
2003-09-12
*
error
herbelin
2003-09-09
*
Export process_module_bindings pour traducteur
herbelin
2003-09-02
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...
herbelin
2003-06-10
*
Déplacement traducteur de nom dans Constrextern pour accès aux noms longs
herbelin
2003-06-10
*
code mort
herbelin
2003-06-10
*
Extension renommage
herbelin
2003-05-20
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
CoqIde : but reset_mod
filliatr
2003-05-19
*
configure et make install s'occupent de CoqIde tout seuls
filliatr
2003-05-19
*
but Require dans une Section
filliatr
2003-05-19
*
table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ...
filliatr
2003-05-15
*
Deplacement lemmes sur fact de Reals vers Arith
herbelin
2003-05-14
*
Orthographe anglaise - typos
herbelin
2003-05-13
*
Orthographe anglaise
herbelin
2003-05-13
*
Corrige Bug (PR#290)
coq
2003-05-05
*
En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...
herbelin
2003-04-29
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
Affichage forcé des implicites contextuels si pas de contexte connu
herbelin
2003-04-10
*
Bug init_function
herbelin
2003-04-09
*
Synchronisation séparée des implicites pour l'affichage du traducteur;
herbelin
2003-04-09
*
Correction Show Implicits
herbelin
2003-04-09
[prev]
[next]