index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
termast.ml
Commit message (
Expand
)
Author
Age
*
Parsing
herbelin
2001-08-10
*
Facilites pour le debogguage des univers.
coq
2001-05-29
*
un warning pas beau supprimmé
filliatr
2001-04-23
*
Bug affichage d'implicites pour les vars liees
herbelin
2001-04-15
*
Bug MUTCASE au lieu CASE
herbelin
2001-03-22
*
entetes
filliatr
2001-03-15
*
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Bug affichage coercions
herbelin
2001-02-16
*
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
*
Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...
herbelin
2001-02-06
*
Suppression de l'affichage des instances des ?n
herbelin
2000-12-18
*
Ajout des Fix et CoFix dans les patterns
delahaye
2000-11-28
*
Prise en compte des implicites de locaux à l'affichage
herbelin
2000-11-27
*
Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;
herbelin
2000-11-23
*
Utilisation de global_reference dans rawconstr
herbelin
2000-11-20
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALIST
herbelin
2000-10-05
*
Utilisation de local_strong plutôt que strong buggé avec défs locales
herbelin
2000-10-04
*
Renommage AppL en App
herbelin
2000-10-01
*
Abstraction de constr
herbelin
2000-09-14
*
Correction pour make doc
herbelin
2000-09-10
*
Suppression de Abst
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
portage Refine
filliatr
2000-07-20
*
Nettoyage de Generic
herbelin
2000-05-31
*
Modification messages d'erreurs, possibilité de n'importe quel constr dans l...
herbelin
2000-05-26
*
Réparation bug d'affichage et affichage des instanciations par des {...}
herbelin
2000-05-23
*
Commentaires
herbelin
2000-05-22
*
suppression de Fw pour les implicites
herbelin
2000-05-03
*
Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'
herbelin
2000-05-02
*
Suite intégration de constr_pattern
herbelin
2000-04-30
*
Déplacement du type reference dans Term
herbelin
2000-04-28
*
Changement de représentation du contexte des réf dans rawconstr et pattern
herbelin
2000-04-28
*
Introduction d'un type constr_pattern pour les différents filtrages
herbelin
2000-04-26
*
Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...
herbelin
2000-03-21
*
Affichage des anonymes si lambda
herbelin
2000-03-20
*
Capture des exceptions si env vide pour ne pas echouer lors du debogage
herbelin
2000-03-07
*
Restructuration printer et parser
herbelin
2000-01-07
*
Nouveaux types 'constructor' et 'inductive' dans Term;
herbelin
1999-12-15
*
Poursuite intégration du Cases
herbelin
1999-12-13
*
Intégration initiale du Cases
herbelin
1999-12-11
*
Suppression Rel de rawconstr et correction de bugs d'affichage
herbelin
1999-12-10
*
Bug affichage constructeur
herbelin
1999-12-09
*
Discharge (encore bugge)
filliatr
1999-12-09
*
mise au point lexer / debugage PP
filliatr
1999-12-05
*
affichage classes et coercions
filliatr
1999-12-02
[next]