aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2007-02-07doc de ring/field + option infinite -> completenessbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9602 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-06Report de la révision 9599 de la v8.1 dans le trunknotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9600 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-06Passage de Set à Type dans Relations et Wellfoundedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9598 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-06doc for fieldthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9596 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-05complement du commit 9591bgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9592 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-05changement dans ring specification du sign, divisionbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9591 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-03Work on ineqs generation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9590 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02Factorisation de la règle Constr.binder dans g_subtac.ml pour éviterherbelin
de cacher l'instance de la règle figurant dans g_constr (report révision 9588 de 8.1 vers trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9589 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02field: introduction de Get_goalbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9587 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02ring: introduction de Get_goalbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9586 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02Now 1/x * x simplifies to 1thery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9585 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Report de révision 9583 de la v8.1 dans le trunknotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9584 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Suppression de code mortnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9582 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Report 9545 de 8.1 vers trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9581 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Petite relecture partie ringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9580 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Report de la révision 9577 dans le trunknotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9578 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-01Abbreviation of order notation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9576 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31report de r9574: doc de fieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9575 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31Correction d'un bug dans check_and_clear_in_constr + simplification denotin
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
2007-01-31MAJ ringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9569 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31Correction typo eq_rec_eq (cf bug #1339)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9567 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31redirection of errors in coqide + dynamic warning printer (needed for tm_egg)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31Fix typo.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9565 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31Fix order of wf and measure arguments, patch Program doc.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9561 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-30Nouvelle implantation de clear_hypsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9560 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-30suite du commit 9557 soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9559 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-30Petite correction sur un message d'erreur renvoyé au sous typage.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9557 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-30constr_of_pat bug with nested patterns.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9556 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29bugfix for suffices (support for open head)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9555 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29Various fixes in subtac, update some test cases.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9553 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29finalized sufficescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9552 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9550 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-28"suffices" implemented + syntax cleanupcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9549 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-28Pas de solution à court terme pour ce problème de complexitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9548 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-26Explication du intros until nnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9543 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-26Contounement d'un probleme avec la VM dans Function jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9538 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-26correction d'un bug d'efficacite dans le printerjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9536 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-25decl mode: anonymous factscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-25Redondance erronée dans les testsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9533 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-24doc de ringbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9532 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-24modifications des messages d'erreurs renvoyés lors de la comparaison soubiran
de deux signatures de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9531 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-24Update some tests and fix section bug.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9530 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-24changement de la fonction norm_substbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9529 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-24Tentative amélioration messages d'erreur prédicat d'élimination (cf notammentherbelin
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
2007-01-24Correction bug #1333 (test non récursivité des dépendances en d'autresherbelin
"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
2007-01-23Updated Makefile to include ConstructiveEpsilon.vemakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9523 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-23Derivation of (exists x : A, P x) -> {x : A | P x} for decidable Pemakarov
and countable A. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9522 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-23ring : Correction du bug PR#1306bgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9520 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-22Correction du bug #1315:notin
- 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
2007-01-22Correction d'un bug d'unification-pattern dans l'algo d'unificationherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 01:45:50 +0000