aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Now 1/x * x simplifies to 1Gravatar thery2007-02-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9585 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de révision 9583 de la v8.1 dans le trunkGravatar notin2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de code mortGravatar notin2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9582 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report 9545 de 8.1 vers trunkGravatar herbelin2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite relecture partie ringGravatar herbelin2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision 9577 dans le trunkGravatar notin2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abbreviation of order notation.Gravatar msozeau2007-02-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9576 85f007b7-540e-0410-9357-904b9bb8a0f7
* report de r9574: doc de fieldGravatar barras2007-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans check_and_clear_in_constr + simplification deGravatar notin2007-01-31
| | | | | | | | la gestion des erreurs dans clear_hyps. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9571 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ ringGravatar herbelin2007-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9569 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction typo eq_rec_eq (cf bug #1339)Gravatar herbelin2007-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9567 85f007b7-540e-0410-9357-904b9bb8a0f7
* redirection of errors in coqide + dynamic warning printer (needed for tm_egg)Gravatar corbinea2007-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typo.Gravatar msozeau2007-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9565 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix order of wf and measure arguments, patch Program doc.Gravatar msozeau2007-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle implantation de clear_hypsGravatar notin2007-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9560 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite du commit 9557 Gravatar soubiran2007-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite correction sur un message d'erreur renvoyé au sous typage.Gravatar soubiran2007-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9557 85f007b7-540e-0410-9357-904b9bb8a0f7
* constr_of_pat bug with nested patterns.Gravatar msozeau2007-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9556 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugfix for suffices (support for open head)Gravatar corbinea2007-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9555 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes in subtac, update some test cases.Gravatar msozeau2007-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9553 85f007b7-540e-0410-9357-904b9bb8a0f7
* finalized sufficesGravatar corbinea2007-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9552 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.Gravatar msozeau2007-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9550 85f007b7-540e-0410-9357-904b9bb8a0f7
* "suffices" implemented + syntax cleanupGravatar corbinea2007-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9549 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas de solution à court terme pour ce problème de complexitéGravatar herbelin2007-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9548 85f007b7-540e-0410-9357-904b9bb8a0f7
* Explication du intros until nGravatar notin2007-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contounement d'un probleme avec la VM dans Function Gravatar jforest2007-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9538 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction d'un bug d'efficacite dans le printerGravatar jforest2007-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9536 85f007b7-540e-0410-9357-904b9bb8a0f7
* decl mode: anonymous factsGravatar corbinea2007-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redondance erronée dans les testsGravatar herbelin2007-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9533 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc de ringGravatar bgregoir2007-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9532 85f007b7-540e-0410-9357-904b9bb8a0f7
* modifications des messages d'erreurs renvoyés lors de la comparaison Gravatar soubiran2007-01-24
| | | | | | | de deux signatures de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9531 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update some tests and fix section bug.Gravatar msozeau2007-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9530 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement de la fonction norm_substGravatar bgregoir2007-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9529 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative amélioration messages d'erreur prédicat d'élimination (cf notammentGravatar herbelin2007-01-24
| | | | | | | rapport de bug #1225 -- qui reste ouvert sur le fond) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9527 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1333 (test non récursivité des dépendances en d'autresGravatar herbelin2007-01-24
| | | | | | | | "library" lors de la construction d'une "library" -- i.e. d'un .vo) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9524 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated Makefile to include ConstructiveEpsilon.vGravatar emakarov2007-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9523 85f007b7-540e-0410-9357-904b9bb8a0f7
* Derivation of (exists x : A, P x) -> {x : A | P x} for decidable PGravatar emakarov2007-01-23
| | | | | | | | and countable A. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9522 85f007b7-540e-0410-9357-904b9bb8a0f7
* ring : Correction du bug PR#1306Gravatar bgregoir2007-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9520 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1315:Gravatar notin2007-01-22
| | | | | | | | | | | | | | | | | | - ajouts des opérations clear_evar_hyps_in_evar, clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui permettent de supprimer des hypothèses dans le contexte des evars, en créant une nouvelle evar avec un contexte restreint; - adaptation de clear_hyps dans Logic pour qu'elle mette à jour le contexte des evars; - adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié; - déplacement de la tactique Change_evars dans prim_rule. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug d'unification-pattern dans l'algo d'unificationGravatar herbelin2007-01-22
| | | | | | | | des tactiques (ne marchait que si l'instance était une application). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9516 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allègement de l'affichage des références par le printer si possibleGravatar herbelin2007-01-22
| | | | | | | | | | | | (on garde des noms de la forme IND(name,i) et CONSTR(name,i,j) que lorsqu'on ne sait pas le bon nom, i.e. pour les IND mutuels autres que le premier et pour tous les constructeurs). Pour un affichage complètement explicite des noms avec ocamldebug, charger maintenant set_raw_db en plus de db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification redondance Axiome du choix unique/descriptionGravatar herbelin2007-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9513 85f007b7-540e-0410-9357-904b9bb8a0f7
* changes in declarative language : by term using tacticGravatar corbinea2007-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9512 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour le rapport de bug #1325 par rétablissement duGravatar herbelin2007-01-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | comportement pré-inductifs polymorphes vis à vis du test d'inclusion des hypothèses de section (i.e. test dans le noyau mais pas dans typing.ml qui est le typeur utilisé généralement par les tactiques). En effet, les variables de section sont vues par les tactiques comme des variables locales qui sont modifiables (p.ex. par conversion). Mais le changement de la signature des variables de section fait échouer le typage noyau (qui exige une égalité syntaxique des types de ces variables) pour les demandes de typage en provenance des tactiques. Quelle est la bonne solution ? - Faut-il comparer les variables de section modulo réduction dans le noyau ? - Faut-il continuer à utiliser un typeur qui ne teste pas les hyps de section pour les tactiques, comme c'était le cas avant les inductifs polymorphes (c'est la solution pragmatique adoptée pour résoudre #1325) - Faut-il éviter la confusion entre variables de section et variables de but ? Incidemment, branchement de Tacmach.hnf_type_of sur Retyping, ce qui, outre des calculs de typage allégés pour les tactiques, évite aussi de tomber sur le comportement du bug #1325. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9510 85f007b7-540e-0410-9357-904b9bb8a0f7
* Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouentGravatar herbelin2007-01-22
| | | | | | | (particulièrement intéressant pour simplify du fait de sa proximité avec simpl) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9508 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des univers algébriques dans les types inférés dansGravatar herbelin2007-01-19
| | | | | | | | | les interfaces de module (bug similaire à #1302 mais pour les définitions -- au lieu des inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de l'afficheur de substitutions de noms de modules pour le débogueurGravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9504 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9503 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tests de référence circulaire au sous-typage de module (pour mémoire)Gravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9501 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-04 09:29:57 +0000