aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.ml
Commit message (Expand)AuthorAge
* module Explore générique et réécriture EAuto avec ce module; occur check ...Gravatar filliatr2001-03-05
* backtrack unification types et deplacement make_clenv_bindingGravatar filliatr2001-03-01
* introduction d'un refine avec resolution des types et de l'instantiation des ...Gravatar mohring2001-02-28
* Retour en arrière sur le pb f_equal en attente meilleure solutionGravatar herbelin2001-01-22
* Bug « f_equal » : arguments inférables par une unification des types qui n...Gravatar herbelin2001-01-21
* Redondant or incompatible instantiations in clenv_assign now correctly trappedGravatar herbelin2000-12-16
* Prise en compte Let dans le calcul des arguments manquants d'un lemme (clenv_...Gravatar herbelin2000-12-05
* Branchement du mécanisme d'instantiation des Evar en présence de définitio...Gravatar herbelin2000-11-27
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
* NettoyageGravatar herbelin2000-11-22
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Chasse au Cast de CastGravatar herbelin2000-10-27
* Renommage canonique :Gravatar herbelin2000-10-18
* Renommage AppL en AppGravatar herbelin2000-10-01
* Plus de whd_castapp_stackGravatar herbelin2000-10-01
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* 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
* Modifs de presentation.Gravatar delahaye2000-06-28
* portage EAuto et RingGravatar filliatr2000-06-21
* Nettoyage de GenericGravatar herbelin2000-05-31
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
* bug (typage avec meta)Gravatar herbelin2000-05-18
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* chgt unify_0Gravatar herbelin2000-04-28
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* Remplacement plain_instance en instance qui n'a plus besoin de envGravatar herbelin2000-03-21
* Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'Gravatar herbelin2000-03-17
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
* bug mk_clenv_from lorsque pas d argumentsGravatar filliatr1999-12-14
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* premier debugageGravatar filliatr1999-12-05
* - coqmktopGravatar filliatr1999-12-03
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* module WcclausenvGravatar filliatr1999-11-22
* - documentation repertoire proofs/Gravatar filliatr1999-10-20
* module Clenv (debut)Gravatar filliatr1999-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 04:04:10 +0000