aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-04use loc instead of dummy_loc in the ugly intro-pattern rewrite hackletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10615 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-02A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)letouzey
... but still no idea why it was working fine on some machines even without this patch... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10614 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-01Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_Oherbelin
(rapport de bug 1807). Cf explication dans le fichier et/ou dans le bug-tracker. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10613 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-01Rework on rich forms of rewriteletouzey
1) changed the semantics of rewrite H,H' : the earlier semantics (rewrite H,H' == rewrite H; rewrite H') was poorly suited for situations where first rewrite H generates side-conditions. New semantics is tclTHENFIRST instead of tclTHEN, that is side-conditions are left untouched. Note to myself: check if side-effect-come-first bug of setoid rewrite is still alive, and do something if yes 2) new syntax for rewriting something many times. This syntax is shamelessly taken from ssreflect: rewrite ?H means "H as many times as possible" (i.e. almost repeat rewrite H, except that possible side-conditions are left apart as in 1) rewrite !H means "at least once" (i.e. rewrite H; repeat rewrite H) rewrite 3?H means "up to 3 times", maybe less (i.e. something like: do 3 (try rewrite H)). rewrite 3!H means "exactly 3 times" (i.e. almost do 3 rewrite H). For instance: rewrite 3?foo, <-2!bar in H1,H2|-* 3) By the way, for a try, I've enabled the syntax +/- as synonyms for ->/<- in the orientation of rewrite. Comments welcome ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10612 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-29Petite modif pour pouvoir faire "intros until 0" qui introduit autant aspiwack
que possible des variables qui ont déjà un nom joli tout plein. La conséquence c'est qu'on peut aussi faire "destruct 0" qui est vachement moins intéressant... Mais bon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10610 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-29Argumentation plus poussée de pourquoi on retire la condition x>0 dansherbelin
Rpower_O alors qu'on la garde pour les autres propriétés de la puissance. (résultat d'une discussion avec Assia et Jean-Marc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10609 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Some suggestions about FMap by P. Casteran: letouzey
- clarifications about Equality on maps Caveat: name change, what used to be Equal is now Equivb - the prefered equality predicate (the new Equal) is declared a setoid equality, along with several morphisms - beginning of a filter/for_all/exists_/partition section in FMapFacts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10608 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Coq_makefile: correction de l'appel aux exécutables Ocamlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10606 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28cardinal is promoted to the rank of primitive member of the FMap interfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10605 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Coq_makefile: Correction d'un bug sur les options passées à Coqdocnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10604 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Do not open type_scope in SetoidClass.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10603 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Fix compilation problem (hopefully).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10602 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Nicer third spec of choose. letouzey
The old version is now a properties in FSetProperties.OrdProperties git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10601 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27For more uniformity, use implicits in FSetAVLletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10600 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27Application patch #1807 sur hypothèse inutile de Rpower_Oherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10599 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27Génération d'une toc en html et avec l'option -psnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10597 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10596 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27Bug dans la génération de la stdlibnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10595 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27Amélioration de la gestion des chemins physiques (corrige au passage le bug ↵notin
#939 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10594 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27patch for C code of addmuldiv31thery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10593 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27typoletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10592 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-26New instance returns the (future) identifier of the instance.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10590 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-26Proper implicit arguments handling for assumptionsmsozeau
(Axiom/Variable...). New tactic clapply to apply unapplied class methods in tactic mode, simple solution to the fact that apply does not work up-to classes yet. Add Functions.v for class definitions related to functional morphisms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-25coq_makefile: variablesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10586 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-25coq_makefile: dépendances + génération des fichiers htmlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10585 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-25Bug de coqdoc : les commentaires simples généraient des lignes videsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10584 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-25Correction d'un bug de Coqdoc (indentation des lignes)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10583 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-25Forgotten file in previous commitlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10581 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-22Merge with lmamane's private branch:lmamane
- New vernac command "Delete" - New vernac command "Undo To" - Added a few hooks used by new contrib/interface - Beta/incomplete version of dependency generation and dumping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-21congruence now knows about _ -> _corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10579 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-20Petits oublis dans Makefile.docnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10578 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-19added products and sorts as possible heads for canonical structurescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10577 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-19fixed pp for declarative modecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10576 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-18Petite correction suite à la révision 10571notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10575 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-18Ajout de caractères unicode reconnus apr le lexernotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10574 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-15Patch bug #1799soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10573 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-15Suppression d'un include et de 2 variables inutilesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10572 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Suspension de l'introduction de delta dans apply : certaines contribsherbelin
qui utilisent apply pour l'automatisation explosent (cf CatsInZFC qui passe de 20mn de compilation à 7h), d'autres instancient les métas par des expressions plus dépliées qu'avant, ce qui conduit à des échecs après coup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10571 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Plongement de doc/Makefile dans la nouvelle architecutre des Makefilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Bug de Coqdoc avec l'option -Rnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10569 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Some bad emacs messup that was commited...msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10568 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Reconnaissance des tokens dans les notations (suite à la revision r10562)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10567 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Added default canonical structures (see example in test-suite)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10566 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Backtrack changes on eauto, move specialized version of eauto inmsozeau
class_tactics for further customizations. Add Equivalence.v for typeclass definitions on equivalences and clrewrite.v test-suite for clrewrite. Debugging the tactic I found missing morphisms that are now in Morphisms.v and removed some that made proof search fail or take too long, not sure it's complete however. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10565 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Move class_setoid to class_tactics.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10564 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Debugging of the class_setoid tactic and eauto. Prepare for move frommsozeau
class_setoid to class_tactics... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10563 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Correction du bug #1512notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10562 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Implement KEEP_ML4_PREPROCESSED option in build systemlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Implement NO_RECALC_DEPS option in build systemlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10560 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 03:06:54 +0000