index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
Commit message (
Expand
)
Author
Age
*
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
herbelin
2006-05-19
*
r8931@thot: notin | 2006-04-28 16:19:38 +0200
notin
2006-04-28
*
Typo dans précédent commit (8755); protection renforcée dans analyse claus...
herbelin
2006-04-28
*
- Distinction explicite des parties paramètres et arguments dans le type
herbelin
2006-04-27
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
préparation de add_glob en vue d'isolement de la partie module pour
herbelin
2006-04-27
*
- Utilisation d'abbréviations pour les types intervenant dans RCases
herbelin
2006-04-26
*
Timide tentative de clarification du statut de l'opérateur de filtrage
herbelin
2006-04-24
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Amendement impression evar pour affichage des Meta par 'info'
herbelin
2006-03-31
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
2006-03-22
*
- Correction bug calcul mind_consnrealargs, introduit à la révision
herbelin
2006-03-22
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
Correction message d'erreur ltac et adoption du modèle de message de Tacinterp
herbelin
2006-03-04
*
Ajout nat_path et find_reference
herbelin
2006-02-04
*
Utilisation du section_path pour le parsing des notations primitives,
herbelin
2006-02-04
*
Adaptation message d'erreur au cas des string
herbelin
2006-01-31
*
Déplacement du test du bon nombre d'argument des constructeurs (et de
herbelin
2006-01-30
*
Nettoyage warning (dont flush et affichage seulement si mode verbose)
herbelin
2006-01-30
*
Bug 'match x in I' (potentiellement utilisable comme cast)
herbelin
2006-01-29
*
exporting the global reference to the inductive " \/ " in coqlib and
bertot
2006-01-25
*
Suppression de la dépendance en Map.fold de ocaml dont la sémantique a
herbelin
2006-01-24
*
Version préliminaire d'inversion de la compilation du filtrage
herbelin
2006-01-16
*
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nom
herbelin
2006-01-16
*
Résidus du traducteur v7 -> v8
herbelin
2006-01-11
*
Résidus du traducteur v7 -> v8
herbelin
2006-01-11
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...
herbelin
2006-01-09
*
Prise en compte, enfin, du contexte des types de retour de ACases et RCases
herbelin
2006-01-08
*
Prise en compte de notations numérales définies au niveau utilisateur + tra...
herbelin
2006-01-08
*
Enregistrement dans glob.dump des utilisations de notations numériques (qui ...
herbelin
2006-01-08
*
Automatisation de l'utilisation de token primitifs dans les motifs de filtrag...
herbelin
2006-01-08
*
Ajout rawconstr_of_aconstr
herbelin
2006-01-08
*
Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ...
herbelin
2006-01-05
*
Suppression des coercions non seulement avant l'affichage des notations mais ...
herbelin
2006-01-04
*
Redéclaration de la notation à l'import pour être cohérent avec l'activat...
herbelin
2006-01-03
*
Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...
herbelin
2005-12-30
*
Ajout booléens; nettoyage
herbelin
2005-12-30
*
Petite correction nom QuantHypArgType suite suppression traducteur
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Simplifification de vernac_expr li l'abandon du traducteur
herbelin
2005-12-23
*
Correction bugs commit précédent
herbelin
2005-12-22
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Changement des named_context
gregoire
2005-12-02
*
Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)
herbelin
2005-11-21
*
Correction de la correction du test sur le nombre de parametres d'une projection
herbelin
2005-11-19
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Types inductifs parametriques
mohring
2005-11-02
*
Conséquences nettoyage pretyping.ml
herbelin
2005-09-09
[next]