aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenv.ml
AgeCommit message (Collapse)Author
2001-12-17Mauvais nom d'erreur d'échec de nthherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2302 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Diverses petites simplications de la machine de preuves.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suppression des stamps et donc des *_constraintsclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-10Incompatibilité entre la prise en compte des univers au niveau des ↵herbelin
tactiques et le test de conversion qui oublie la cumulativité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2107 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-17unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec lesbarras
sous-termes de (plus O O) ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1975 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10Un conv aurait dû être un conv_leqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1945 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Suppression du retypage dans w_Declareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1933 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-29Autoriser Apply avec un but sous forme d'implication ou de quantificationbarras
universelle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1817 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05module Explore générique et réécriture EAuto avec ce module; occur check ↵filliatr
dans clenv_merge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1425 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01backtrack unification types et deplacement make_clenv_bindingfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1417 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28introduction d'un refine avec resolution des types et de l'instantiation des ↵mohring
metas dans les existentielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1415 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-22Retour en arrière sur le pb f_equal en attente meilleure solutionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1265 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-21Bug « f_equal » : arguments inférables par une unification des types qui ↵herbelin
n'était pas faite (rem: le nouveau test ralentit un peu l'ensemble) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1263 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Redondant or incompatible instantiations in clenv_assign now correctly trappedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1136 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Prise en compte Let dans le calcul des arguments manquants d'un lemme ↵herbelin
(clenv_environments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1051 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Branchement du mécanisme d'instantiation des Evar en présence de ↵herbelin
définitions locales vers Evarutil git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@970 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@923 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Reparation IsMutConstruct + Transparentmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@920 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@918 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
de fonctions dans les .vo ajout de lemmes dans EqNat, Logic_Type suppression de PolyListSyntax qui redefinissait le Infix de append Recherche d'instances a reecrire dans les Cases et les FixPoint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@820 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-02suppression des (* open Generic *)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27Chasse au Cast de Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@776 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Renommage canonique :herbelin
declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en Appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Plus de whd_castapp_stackherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@623 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-26Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion ↵herbelin
de 'OpenConstr' constitué d'un terme avec Métas et d'une liste de types pour les métas git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@615 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Correction pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Suppression de Abstherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-28Modifs de presentation.delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@520 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21portage EAuto et Ringfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@513 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Nettoyage de Genericherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-25Bug existential_value au lieu de existential_type + divers sur existentialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@476 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18bug (typage avec meta)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@455 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@442 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Ajout du langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28chgt unify_0herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@378 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@368 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Remplacement plain_instance en instance qui n'a plus besoin de envherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@340 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-17Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@322 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 19:13:20 +0000