index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
pretyping.ml
Commit message (
Expand
)
Author
Age
*
- Débogueur: positionnement de set_detype_anonymous pour ne pas
herbelin
2007-08-29
*
Suppression des type_app et body_of_type qui alourdissent inutilement le code
herbelin
2007-08-27
*
If a fixpoint is not written with an explicit { struct ... }, then
letouzey
2007-07-07
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2007-03-15
*
Protection contre une source possible de liaison de lambda anonyme
herbelin
2006-12-29
*
Suppression source de complexité polynomiale introduite par le polymorphisme
herbelin
2006-11-03
*
Compatibilité du polymorphisme de constantes avec les sections.
herbelin
2006-10-29
*
Remplacement des nf_evar (source de complexité polynomiale) par de la
herbelin
2006-10-06
*
Suppression d'une source de complexité polynomiale dans le pretypage
herbelin
2006-10-06
*
Report de l'heuristique d'unification premier ordre flexible/rigide
herbelin
2006-09-15
*
Export de check_evars vers command.ml
herbelin
2006-09-01
*
Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...
herbelin
2006-06-27
*
The "clean integration of subtac" patch.
msozeau
2006-05-29
*
- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites
herbelin
2006-05-28
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
Fixes for new unification, not used in default version as it really changes u...
msozeau
2006-04-10
*
Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...
msozeau
2006-04-10
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Inductifs avec polymorphisme de sorte (version initiale)
herbelin
2006-03-29
*
Subtac fixes, single fixpoint definitions are working again. Added a toggle o...
msozeau
2006-03-22
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
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
*
Localisation des erreurs de sorte du prétypage
herbelin
2006-02-08
*
Suppression résidus code v7 et traducteur
herbelin
2006-01-11
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Changement des named_context
gregoire
2005-12-02
*
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
*
Léger nettoyage et uniformisation + généralisation du point d'entrée ltac...
herbelin
2005-09-09
*
reparations de quelques petits bugs d\'unification + introduction de la notio...
barras
2005-06-07
*
essai de typage des instantiations d\'evars
barras
2005-06-06
*
Backtrack sur la substitution combinée avec l'instanciation en réponse à l...
herbelin
2005-03-15
*
A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...
herbelin
2005-03-10
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
Correction de la précédence des contexts de variables rel, ltac et var
herbelin
2005-02-02
*
Relâchement obligation d'une contrainte de type sur les Hole en position ter...
herbelin
2004-12-06
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...
herbelin
2004-08-24
*
Nouvelle en-tête
herbelin
2004-07-16
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
Prise en compte d'un type dont la sorte est une evar
herbelin
2004-04-29
*
Correction incapacité à gérer les annotations de type dépendantes pour le...
herbelin
2004-04-27
*
Typo
herbelin
2004-03-29
[next]