aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* - Débogueur: positionnement de set_detype_anonymous pour ne pasGravatar herbelin2007-08-29
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* If a fixpoint is not written with an explicit { struct ... }, then Gravatar letouzey2007-07-07
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Protection contre une source possible de liaison de lambda anonymeGravatar herbelin2006-12-29
* Suppression source de complexité polynomiale introduite par le polymorphismeGravatar herbelin2006-11-03
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Remplacement des nf_evar (source de complexité polynomiale) par de laGravatar herbelin2006-10-06
* Suppression d'une source de complexité polynomiale dans le pretypageGravatar herbelin2006-10-06
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* Export de check_evars vers command.mlGravatar herbelin2006-09-01
* Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...Gravatar herbelin2006-06-27
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
* Fixes for new unification, not used in default version as it really changes u...Gravatar msozeau2006-04-10
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...Gravatar msozeau2006-04-10
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* Subtac fixes, single fixpoint definitions are working again. Added a toggle o...Gravatar msozeau2006-03-22
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* Correction message d'erreur ltac et adoption du modèle de message de TacinterpGravatar herbelin2006-03-04
* Localisation des erreurs de sorte du prétypageGravatar herbelin2006-02-08
* Suppression résidus code v7 et traducteurGravatar herbelin2006-01-11
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Léger nettoyage et uniformisation + généralisation du point d'entrée ltac...Gravatar herbelin2005-09-09
* reparations de quelques petits bugs d\'unification + introduction de la notio...Gravatar barras2005-06-07
* essai de typage des instantiations d\'evarsGravatar barras2005-06-06
* Backtrack sur la substitution combinée avec l'instanciation en réponse à l...Gravatar herbelin2005-03-15
* A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...Gravatar herbelin2005-03-10
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* Correction de la précédence des contexts de variables rel, ltac et varGravatar herbelin2005-02-02
* Relâchement obligation d'une contrainte de type sur les Hole en position ter...Gravatar herbelin2004-12-06
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...Gravatar herbelin2004-08-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* Prise en compte d'un type dont la sorte est une evarGravatar herbelin2004-04-29
* Correction incapacité à gérer les annotations de type dépendantes pour le...Gravatar herbelin2004-04-27