aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Expand)AuthorAge
* Unification plus efficace vis à vis du LetInGravatar herbelin2003-01-31
* reparation des contribs: lors de l'unification, reduire les beta redexesGravatar barras2003-01-23
* modified the unification algorithm to try first order unification beforeGravatar barras2003-01-22
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* L'ordre supérieur avait quelque peu été oublié dans l'unification...Gravatar herbelin2002-06-07
* Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...Gravatar herbelin2002-04-11
* Amélioration des messages d'erreurs concernant l'inférence des implicitesGravatar herbelin2002-04-10
* bug #134: on appelait solve_simple_eqn avec une evar qui etait resolueGravatar barras2002-02-18
* GROS COMMIT:Gravatar barras2001-11-05
* Amérioration message d'erreur en cas d'échec du filtrage de premier ordreGravatar herbelin2001-10-29
* Nettoyage Recordobj et conséquencesGravatar herbelin2001-10-16
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* la conversion ne doit être testé dans evar_conv qu'en absence de evarGravatar herbelin2001-07-06
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Modification pour passage p-automatesGravatar mohring2001-05-15
* Changement de la structure des points fixesGravatar barras2001-05-03
* Bug context incoherent au passage du lambda et du let dans evar_eqapprGravatar herbelin2001-04-10
* amelioration de la structure des universGravatar barras2001-03-28
* amelioration de la consommation memoire de la conversion en eta-expansantGravatar barras2001-03-23
* entetesGravatar filliatr2001-03-15
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Bug de contextesGravatar herbelin2000-12-26
* Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...Gravatar herbelin2000-12-26
* Utilisation de Let In pour les constantes locales, prise en compte des Let In...Gravatar herbelin2000-11-27
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Petit nettoyage de Evarutil et EvarconvGravatar herbelin2000-10-23
* 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
* Suppression de AbstGravatar 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
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Reparation bug isevars dans pretypingGravatar herbelin2000-03-10
* Poursuite intégration du CasesGravatar herbelin1999-12-13
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* portage modules Evarconv et EvarutilGravatar filliatr1999-11-29
* Versions initialesGravatar herbelin1999-11-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-07 18:14:49 +0000