aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
AgeCommit message (Expand)Author
2006-09-01Export de check_evars vers command.mlherbelin
2006-06-27Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...herbelin
2006-05-29The "clean integration of subtac" patch.msozeau
2006-05-28- Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesherbelin
2006-04-28Standardisation du nom des méthodes de Evdherbelin
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-04-14Si un fixpoint a plusieurs arguments, mais un seul de type inductif, letouzey
2006-04-10Fixes for new unification, not used in default version as it really changes u...msozeau
2006-04-10Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...msozeau
2006-04-07- Documentation of the Program tactics.msozeau
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
2006-03-22Subtac fixes, single fixpoint definitions are working again. Added a toggle o...msozeau
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau
2006-03-04Correction message d'erreur ltac et adoption du modèle de message de Tacinterpherbelin
2006-02-08Localisation des erreurs de sorte du prétypageherbelin
2006-01-11Suppression résidus code v7 et traducteurherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-02Types inductifs parametriquesmohring
2005-09-09Léger nettoyage et uniformisation + généralisation du point d'entrée ltac...herbelin
2005-06-07reparations de quelques petits bugs d\'unification + introduction de la notio...barras
2005-06-06essai de typage des instantiations d\'evarsbarras
2005-03-15Backtrack sur la substitution combinée avec l'instanciation en réponse à l...herbelin
2005-03-10A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...herbelin
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-02-02Correction de la précédence des contexts de variables rel, ltac et varherbelin
2004-12-06Relâchement obligation d'une contrainte de type sur les Hole en position ter...herbelin
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-08-24Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-06-25correspondance des records et noms de champs de records entre un module et sa...letouzey
2004-04-29Prise en compte d'un type dont la sorte est une evarherbelin
2004-04-27Correction incapacité à gérer les annotations de type dépendantes pour le...herbelin
2004-03-29Typoherbelin
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...herbelin
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts fix...barras
2004-02-04Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...herbelin
2004-02-03Backtrack sur recuperation de noms a partir du type, car casse la correction ...herbelin
2004-01-29Reparation d'une rupture (en presence de types implicites) de l'invariant que...herbelin
2003-12-19Substitution dans REvar et PEvar plutot que encodage via noeud application po...herbelin
2003-11-19Deplacement subst_rawconstr dans Rawtermherbelin
2003-11-04Amelioration message d'erreur pour ltacherbelin
2003-09-29Oubli du type du terme a filtrer quand pas d'argument dans la traduction de caseherbelin
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom indépen...herbelin
2003-09-10Bug predicat old Caseherbelin