index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
declare.ml
Commit message (
Expand
)
Author
Age
...
*
Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...
herbelin
2001-09-10
*
Légère modification lookup_eliminator
herbelin
2001-09-09
*
Mécanisme pour faire remonter les contraintes de typage sur les variables de...
herbelin
2001-09-09
*
Suppression des library roots, on teste si un nom est absolu autrement
herbelin
2001-09-07
*
Hack rapide pour réduire significativement la taille des vo
herbelin
2001-08-10
*
Parsing
herbelin
2001-08-10
*
Ajout make_elimination_ident
herbelin
2001-08-01
*
Interdiction de faire 2 variables de même nom court
herbelin
2001-07-05
*
correction bug Omega
filliatr
2001-07-05
*
construct_reference regarde d'abord dans le contexte local, puis les globaux
filliatr
2001-05-11
*
utilisation de Options.if_verbose
filliatr
2001-04-03
*
La strategie de recherche de lookup_eliminator etait insuffisante
herbelin
2001-03-23
*
entetes
filliatr
2001-03-15
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Meilleur traitement des noms explicites dans la Nametab; Différentation du t...
herbelin
2001-02-05
*
Remplacement d'un bug non documente par un autre documente dans quantify_extr...
herbelin
2001-01-25
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Réorganisation suite ajout de constantes locales dans les Records
herbelin
2001-01-24
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
find_section_variable : un traducteur id -> sp pour variables de section; var...
herbelin
2000-12-25
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de l...
herbelin
2000-12-05
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
Les variables doivent persister dans les vo pour HELM
herbelin
2000-11-28
*
Bug dans find_common_hyps_then_abstract en présence de défs locales
herbelin
2000-11-27
*
Bug extract_instance en présence de défs locales
herbelin
2000-11-27
*
Prise en compte des let in dans les instances de globaux
herbelin
2000-11-27
*
Nettoyage
herbelin
2000-11-26
*
Prise en compte de noms absolus dans la nametab + nettoyage
herbelin
2000-11-26
*
Bug relocation des hypothèses quand les contextes de définitions et d'utili...
herbelin
2000-11-24
*
Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab
filliatr
2000-11-24
*
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
2000-11-24
*
implicites manuels
filliatr
2000-11-21
*
separation calcul des implicites et declaration des constantes / inductifs / ...
filliatr
2000-11-21
*
Nouveaux points d'accès pour les noms qualifiés
herbelin
2000-11-20
*
methode export
filliatr
2000-11-15
*
Renommage canonique SectionLocalDecl -> SectionLocalAssum
herbelin
2000-11-09
*
out_variable (Liboject.obj -> ...) distibgue de get_variable
filliatr
2000-11-08
*
Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...
herbelin
2000-11-06
*
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr
2000-11-06
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Renommage canonique :
herbelin
2000-10-18
*
Disparition du type oper mais nouveau type global_reference
herbelin
2000-10-01
*
Abstraction de constr
herbelin
2000-09-14
*
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
herbelin
2000-09-12
*
Correction pour make doc
herbelin
2000-09-10
[prev]
[next]