aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.ml
Commit message (Collapse)AuthorAge
* Réparation bug de l'unification. En effet, avant l'instanciation d'une evarGravatar clrenard2003-03-28
| | | | | | | on n'unifiait pas les types ce qui est maintenant fait. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3800 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration choix des noms dans abstract_list_allGravatar herbelin2002-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3485 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2002-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative d'interdire les K-abstractions si allow_K est faux et leGravatar herbelin2002-12-23
| | | | | | | motif n'a pas de métas (dans unify_to_subterm_list) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3479 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cas motif universelGravatar herbelin2002-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3476 85f007b7-540e-0410-9357-904b9bb8a0f7
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des coercions dans les 'with' bindingsGravatar herbelin2002-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3468 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite du commit precedentGravatar barras2002-12-19
| | | | | | | | - amelioration des messages d'erreurs de la condition de garde - reorganisation de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3457 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compensation de suppression betaiota de type_of (suite)Gravatar herbelin2002-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compensation de suppression betaiota de type_of (suite)Gravatar herbelin2002-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compensation de suppression betaiota de type_ofGravatar herbelin2002-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3421 85f007b7-540e-0410-9357-904b9bb8a0f7
* retour en arriere concernant la recherche d'occurence modulo expansion des ↵Gravatar barras2002-10-09
| | | | | | letins, ce qui conduisait a des comportement peu intuitifs. On priviligiera l'utilisation de la tactique Subst. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vraie substitutivite de autohintsGravatar coq2002-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
* modification de clenv_merge:Gravatar barras2002-05-14
| | | | | | | | | on ajoute en premier lieu les contraintes concernant le terme puis apres celles concernant le type de chaque instantiation, au lieu d'alterner l'ajout de contraintes de terme et de type. A l'essai. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2682 85f007b7-540e-0410-9357-904b9bb8a0f7
* typed unification in the case of PatternGravatar barras2002-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2654 85f007b7-540e-0410-9357-904b9bb8a0f7
* backtrack unificationGravatar barras2002-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-introduction de clenv_constrain_missing_arg utilisé par la contrib LannionGravatar herbelin2002-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlGravatar herbelin2002-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2632 85f007b7-540e-0410-9357-904b9bb8a0f7
* backtrack dans l'algo d'unificationGravatar barras2002-04-10
| | | | | | | fichier usage incorrect (libdir et bindir ont disparu) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2629 85f007b7-540e-0410-9357-904b9bb8a0f7
* resolution du pb d'efficacite du a Sign.add_named_declGravatar barras2002-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
* transformation des evar en meta preserve la linearite des metasGravatar barras2002-04-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2605 85f007b7-540e-0410-9357-904b9bb8a0f7
* - modifs de la condition de garde pour mieux tenir compte des raisonnementsGravatar barras2002-04-02
| | | | | | | | | | par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
* backtrack de l'unificationGravatar barras2002-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2562 85f007b7-540e-0410-9357-904b9bb8a0f7
* encore quelques petites modif de l'unificationGravatar barras2002-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2553 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation du pb de conversion dans clenv_unifyGravatar herbelin2002-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2526 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage de fonctionsGravatar barras2002-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2521 85f007b7-540e-0410-9357-904b9bb8a0f7
* unification faite de gauche a droite (et non pas l'inverse) pour eviter queGravatar barras2002-03-05
| | | | | | | clenv_typed_unify plante trop facilement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2511 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2002-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2509 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalisation de l'utilisation de l'unification d'ordre 2Gravatar barras2002-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2498 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
| | | | | | | | + Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
* petite modif pour ne pas expanser trop de let pendant l'unificationGravatar barras2002-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mauvais nom d'erreur d'échec de nthGravatar herbelin2001-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2302 85f007b7-540e-0410-9357-904b9bb8a0f7
* compat ocaml 3.03Gravatar filliatr2001-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-11-05
| | | | | | | | | | - 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
* Incompatibilité entre la prise en compte des univers au niveau des ↵Gravatar herbelin2001-10-10
| | | | | | 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
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
* unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec lesGravatar barras2001-09-17
| | | | | | | sous-termes de (plus O O) ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un conv aurait dû être un conv_leqGravatar herbelin2001-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1945 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression du retypage dans w_DeclareGravatar herbelin2001-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1933 85f007b7-540e-0410-9357-904b9bb8a0f7
* Autoriser Apply avec un but sous forme d'implication ou de quantificationGravatar barras2001-06-29
| | | | | | | universelle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1817 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
| | | | | | | 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
* Changement de la structure des points fixesGravatar barras2001-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration de la structure des universGravatar barras2001-03-28
| | | | | | | | 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
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Explore générique et réécriture EAuto avec ce module; occur check ↵Gravatar filliatr2001-03-05
| | | | | | dans clenv_merge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1425 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-20 14:27:44 +0000