aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
Commit message (Expand)AuthorAge
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* Le calcul de la classe dans class_args_of ne suivait pas celui de class_ofGravatar herbelin2006-10-21
* Correction d'un vieux bug de coercion avec éta-expansion (utilisationGravatar herbelin2006-10-21
* Remplacement des nf_evar (source de complexité polynomiale) par de laGravatar herbelin2006-10-06
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* 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
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* Localisation des erreurs de sorte du prétypageGravatar herbelin2006-02-08
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* 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
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...Gravatar herbelin2002-04-11
* Mise en place de coercion dans les motifsGravatar herbelin2001-12-11
* GROS COMMIT:Gravatar barras2001-11-05
* L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...Gravatar herbelin2001-09-14
* bug de BruijnGravatar herbelin2001-08-13
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Restructuration de classops; évolution en une version mieux intégrée au re...Gravatar herbelin2001-02-05
* Bug environnementGravatar herbelin2001-01-11
* Insertion de coercion au milieu des applications partielles et propagation de...Gravatar herbelin2000-11-08
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Petit nettoyage de Evarutil et EvarconvGravatar herbelin2000-10-23
* Nettoyage CoercionGravatar herbelin2000-10-19
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Renommage AppL en AppGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Achèvement abstraction du mécanisme (optionnel) de castGravatar herbelin2000-06-29
* Amelioration messages erreursGravatar herbelin2000-06-09
* bugs et simplification (suite)Gravatar herbelin2000-06-02
* Bugs et simplifications coercionsGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Afficahge des locationsGravatar herbelin2000-05-31
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Export inh_conv_coerce_to et diversGravatar herbelin2000-03-07
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* - méthode load sur les HintsGravatar filliatr1999-12-13
* mise a jour CoercionGravatar filliatr1999-12-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 02:24:53 +0000