aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Re-essai de forcer le terme réécrit à apparaître dans le butGravatar herbelin2002-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3480 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
* Prise en compte application partielle dans dependentGravatar herbelin2002-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3478 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3477 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
* Backtrack sur la tentative d'interdire les K-abstractions dans l'unificationGravatar herbelin2002-12-21
| | | | | | | faite par Rewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3475 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
* Affinement affichageGravatar herbelin2002-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3473 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2002-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affinement affichageGravatar herbelin2002-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de notation cablees dans 'annot'Gravatar herbelin2002-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3470 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3469 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
* majGravatar filliatr2002-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit netoyage dans libGravatar coq2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression de l'archive cvs d'un bout de debugGravatar letouzey2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3462 85f007b7-540e-0410-9357-904b9bb8a0f7
* les empty ind et les singletons etaient oublies par add_recursorsGravatar letouzey2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3461 85f007b7-540e-0410-9357-904b9bb8a0f7
* apres correction du probleme de Global.env, retour du mis_constr_nargs_envGravatar letouzey2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3460 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug: Global.env() executé au chargement -> eta-expansionGravatar letouzey2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3459 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplification de solve_subgoal: n'utilise plus frontierGravatar barras2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3458 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
* majGravatar filliatr2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3456 85f007b7-540e-0410-9357-904b9bb8a0f7
* - amelioration des messages d'erreur de la condition de gardeGravatar barras2002-12-18
| | | | | | | - restructuration de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3455 85f007b7-540e-0410-9357-904b9bb8a0f7
* stupide inlining des construsteursGravatar letouzey2002-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3454 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contexte locale non-vide interdit a la fin d'un module ou module typeGravatar coq2002-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3453 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3452 85f007b7-540e-0410-9357-904b9bb8a0f7
* exemple complet de parserGravatar barras2002-12-17
| | | | | | | | changement de syntaxe des scope: expr % id ex: (10 + 5 * 4)%N ou 4%N git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3451 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouveau Subst:Gravatar barras2002-12-17
| | | | | | | | - marche lorsqu'il n'y rien a reecrire - marche avec les hypotheses definies (Subst inclut l'Unfold partout) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3450 85f007b7-540e-0410-9357-904b9bb8a0f7
* ma bidouille marche pas...Gravatar letouzey2002-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit netoyage des open's et commentairesGravatar coq2002-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3448 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3447 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une entrée spéciale "annot" pour les piquantsGravatar herbelin2002-12-15
| | | | | | | Positionnement du scope type_scope à certains endroits bien choisis git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout syntaxe '>'Gravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3444 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traitement spécial pour les types à l'internalisationGravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3443 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout "Locate Notation"Gravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des scopes traversés dans les notationsGravatar herbelin2002-12-15
| | | | | | | | Traitement spécial pour le scope type_scope à l'internalisation Ajout "Locate Notation" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleure factorisation des entrées NEXT internesGravatar herbelin2002-12-15
| | | | | | | | Nouvelle entrée "annot" pour contourner le conflit entre ">" et les annotations entre piquants git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxeGravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas de 0 dans positiveGravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout syntaxe '>'Gravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas d'associativite pour =_DGravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3436 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evaluation paresseuse de l'affichage du debugGravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3435 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3434 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
* debut de parcours des modulesGravatar letouzey2002-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3432 85f007b7-540e-0410-9357-904b9bb8a0f7
* une branche de case inutileGravatar letouzey2002-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3431 85f007b7-540e-0410-9357-904b9bb8a0f7
* possibilité de faire Print M avec M module ou modtype au lieu de Print ↵Gravatar letouzey2002-12-13
| | | | | | Module et Print Module Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3430 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant ↵Gravatar letouzey2002-12-13
| | | | | | quand meme Global.env() git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3429 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3428 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-26 20:15:48 +0000