aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Réparation absence d'interprétation des liaisons vers listesGravatar herbelin2007-02-15
| | | | | | | d'occurrences (clause "at") dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9648 85f007b7-540e-0410-9357-904b9bb8a0f7
* encodage des typesGravatar filliatr2007-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9646 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactique yicesGravatar filliatr2007-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9645 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
| | | | | | | | fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug mineur dans la generation des principes d'induction pour FunctionGravatar jforest2007-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9643 85f007b7-540e-0410-9357-904b9bb8a0f7
* Autres passages de Set à Type dans Relations et WellfoundedGravatar herbelin2007-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix matching on dependent types, taking a safe stand.Gravatar msozeau2007-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9641 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans la génération des principes d'inductionGravatar jforest2007-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add keywords that were missing, notably for terms.Gravatar msozeau2007-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9638 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppresion de la catégorie des inductifs singletons larges dontGravatar herbelin2007-02-09
| | | | | | | | l'élimination vers Set était autorisée: comme souligné par Benjamin, c'est incompatible avec EM + AC (report rev 9633 8.1) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9634 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugfix sufficesGravatar corbinea2007-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9632 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour r9310 en attendant mieuxGravatar herbelin2007-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9629 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision r9605 de la branche v8.1 vers le trunk (abstract ↵Gravatar notin2007-02-09
| | | | | | récupère toutes les exceptions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Separate Tactics in subtac.Gravatar msozeau2007-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9627 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add lif then else for if in bool.Gravatar msozeau2007-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix myinjection tactic, generalize coercion for applicationsGravatar msozeau2007-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9625 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix mistake naming my Tactics file Tactics :)Gravatar msozeau2007-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add tactics for induction on subterms.Gravatar msozeau2007-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleur anglais (cf 9619)Gravatar herbelin2007-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification que toutes les evars ont étés instanciées dans les types ↵Gravatar herbelin2007-02-07
| | | | | | implicites des Fixpoint/CoFixpoint (report revision 9617 de 8.1 vers trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1364 (les variables de section sont repérées parGravatar herbelin2007-02-07
| | | | | | | | | interp_var : ne pas les repérer à nouveau comme objets globaux, puisqu'elles ont pu être effacées dans un contexte local de but). (report revision 9611 de la branche 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relecture/nettoyage chapitre Gallina; déplacement section FunctionGravatar herbelin2007-02-07
| | | | | | | | | dans extensions de Gallina. Divers. (report revisions 9614 et 9594 de la branche 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression RefMan-cas.tex inutiliséGravatar herbelin2007-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9613 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur le passage de Set à Type pour l'ordre lexicographiqueGravatar herbelin2007-02-07
| | | | | | | | pour garder Relation_Operators.Pow dans Set (puisque le polymorphisme d'univers pour les inductifs ne se propage pas aux définitions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various subtac fixes. Add inequalities in pattern matching branches when ↵Gravatar msozeau2007-02-07
| | | | | | needed, handle undo for the default tactic... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Field rewrites only with polynomialGravatar thery2007-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9607 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc de ring/field + option infinite -> completenessGravatar barras2007-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision 9599 de la v8.1 dans le trunkGravatar notin2007-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage de Set à Type dans Relations et WellfoundedGravatar herbelin2007-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9598 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc for fieldGravatar thery2007-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9596 85f007b7-540e-0410-9357-904b9bb8a0f7
* complement du commit 9591Gravatar bgregoir2007-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9592 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement dans ring specification du sign, divisionGravatar bgregoir2007-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Work on ineqs generation.Gravatar msozeau2007-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation de la règle Constr.binder dans g_subtac.ml pour éviterGravatar herbelin2007-02-02
| | | | | | | | | 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
* field: introduction de Get_goalGravatar bgregoir2007-02-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9587 85f007b7-540e-0410-9357-904b9bb8a0f7
* ring: introduction de Get_goalGravatar bgregoir2007-02-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9586 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 21:39:41 +0000