aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
Commit message (Expand)AuthorAge
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* Various improvements in handling of evars in general and typingGravatar msozeau2008-06-21
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* 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