aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-04-16Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)letouzey
This way, no more references to NBinDefs.N when doing "Print N". Long-term migration to theories/Numbers is still planned, but it needs more works, for instance to adapt both positive and N and Z at once. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10806 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-16first-order --> firstorder (kills a warning about not being a valid id)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10805 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-16flottantsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10804 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-16Added a function that escapes XML characters in ppcmds.cek
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10803 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15More renamings to avoid clashes (e.g. with CoRN).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10802 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15Mises à jour bugs, CHANGES, code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10801 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15Document CHANGES in setoid rewrite, move DefaultRelation tomsozeau
SetoidTactics and document it. Cleanup Classes.Equivalence. Minor fixes to the Program doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10799 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15* added a subsection to explain the automatic declaration of schemes:vsiles
* Set\Unset Elimination Schemes to switch on/off the declaration of standard elimination schemes * Set\Unset Equality Scheme to switch on/off the declaration of the boolean equality * added a \Rem in injection to explain that if we managed to get a boolean equality, injection can finally work well with dependant pairs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10798 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
semantics. - Add an Equivalence instance for pointwise equality from an Equivalence on the codomain of a function type, used by default when comparing functions with the Setoid's ===/equiv. - Partially fix the auto hint database "add" function where the exact same lemma could be added twice (happens when doing load for example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10797 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
- Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15typovsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10795 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15fix some bogus calls to id_of_string by the extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10794 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-14BinPos: New version of ~1 and ~0 notations, xH replaced by 1 and proofs cleanupletouzey
As suggested by Hugo, Notation "p ~ 1" instead of Notation "p ~1" avoids potential conflict with stuff like ~1=1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10793 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-14oubli sur 10790herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10792 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-14suite 10790 (identificateurs)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10791 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-14Diverses corrections herbelin
- gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev] - suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des quotations de tactiques pour simuler les métas des constr - quitte à devoir utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics] - utilisation de error en place d'un "print_string" d'échec dans fourier - améliorations espérées vis à vis de quelques "bizarreries" dans la gestion des Meta [pretyping] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10790 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-14Update doc and remove another overloading of equiv_*.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10788 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-14Renamings to avoid clashes with definitions in Relation_Definitions, nowmsozeau
projections are of the form "equivalence_reflexive" and instance names too. As they are (almost) never used directly, it does not hurt to have long explicit names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10787 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-14Fix setoid tests, use red for a Setoid_Theory lemma, and Parametricmsozeau
Relation for function spaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10786 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
- vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-12Désactivation du dumping des notations quand funind appelle lesherbelin
commandes d'interprétation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10784 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-12Document the new setoid rewrite tactic, and fix a few things whilemsozeau
testing: - better? pretty printing - correct handling of load/open/cache - do less reduction in build_signature, commited in previous patch. May break some scripts (but Parametric will break more and before :). - remove ===def notation as suggested by A. Spiwack. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10783 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-12Add the ability to specify what to do with free variables in instancemsozeau
declarations. By default, print the list of implicitely generalized variables. Implement new commands Add Parametric Relation/Morphism for... parametric relations and morphisms. Now the Add * commands are strict about free vars and will fail if there remain some. Parametric just allows to give a variable context. Also, correct a bug in generalization of implicits that ordered the variables in the wrong order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10782 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-12Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.msozeau
Uses setoid_rewrite even if rewriting with leibniz if there are specified occurences, maybe a combination of pattern and rewrite could be done instead. Correct spelling of occurrences. Coq does not compile with this patch, the next one will make it compile again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10781 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-11Check that no evars remain in instance types earlier at Instancemsozeau
declarations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10779 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-09Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicitmsozeau
loading and exporting of Setoid to ROmega which uses it for iff. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10775 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-09Verify Setoid is loaded before doing anything.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10774 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-09Fixes in new Morphisms files. msozeau
- Use a notation for predicate instead of a definition (better pretty-printing this way, and no delta problem!). - Correct inadvertent import of Coq.Program.Program which sets implicit arguments for left,right and so on. Should fix the contribs that used to compile. - Correct normalization_tac to do normalization of "inverse" signatures. Add a missing instance, and name the existing ones. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10773 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-09Fix evar bugs in type classes:msozeau
- disallow uninstantiated hypotheses (typically local variables with no assigned types) as solutions for typeclass instantiation. - Fix resolve_typeclasses call in pretyping that was not propagating found instances in the term. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10772 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-09contradict can now handle False hypothesis in the spirit of contradictionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10771 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-09Correction bug List.map2 dans Case12.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10770 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-09Fix the last compilation problemmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10769 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-09Fix compilation problemmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10768 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-08correction of bug 1829jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10766 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
relf/sym/trans relations from morphisms on prop connectives and relations. - Add general order theory on predicates, instantiated for relations. Derives equivalence, implication, conjunction and disjunction as liftings from propositional connectives. Can be used for n-ary homogeneous predicates thanks to a bit of metaprogramming with lists of types. - Rebind Setoid_Theory to use the Equivalence record type instead of declaring an isomorphic one. One needs to do "red" after constructor to get the same statements when building objects of type Setoid_Theory, so scripts break. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10765 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-08Ajout d'options a coqdoc pour l'entete htmlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10764 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-07Fix big de Bruijn bug in mutually recursive definitions.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10763 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-06Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :herbelin
- si on met Rle_ge et Rge_le tous les deux en Resolve (et de même pour Rlt_gt et Rgt_lt) alors on introduit un cycle, - si on en met un des deux en Immediate, alors on perd la symétrie car si un développement n'a un lemme en hints que pour Rge (resp Rle), alors il ne sera pas utilisable si on met Rge_le (resp Rle_ge) en Immediate (et c'est ce qui arrive notamment dans HighSchoolGeometry). L'idéal serait d'introduire une notion de raisonnement modulo équivalence dans auto afin que chaque lemme sur Rle (resp Rge) soit systématiquement applicable aussi face à Rge (resp Rle) sans redondances et sans cycle. Ainsi Rle_ge and co n'auraient pas un statut de hints mais plutôt un statut de conversions implicites entre notions synonymes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10762 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-05Suite 10760herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10761 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-05- Retour en arrière sur la capacité du nouvel apply à utiliser lesherbelin
lemmes se terminant par False ou not sur n'importe quelle formule (cela crée trop d'incompatibilités dans les "try apply" etc.); de toutes façons, "contradict" joue presque ce rôle (à ceci près qu'il ne traverse pas les conjonctions) (tactics/tactics.ml). - Quelques corrections sur RIneq.v - le hint Rlt_not_eq avait été oublié dans la phase de restructuration, - davantage de noms canoniques (O -> 0, etc.), - nouvelle tentative de ramener "auto" vers Rle (avec Rle_ge) plutôt que vers Rge qui est moins souvent associé à des hints. - Utilisation du formateur deep_ft pour afficher les scripts de preuve afin d'éviter le besoin d'un "Set Printing Depth" (vernacentries.ml). - Suppression de certaines utilisations de l'Anomaly de meta_fvalue qui ne correspondaient pas à des comportements anormaux (reductionops.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10760 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-05Minor fixes: msozeau
- Allow unicode superscripts characters. - Put Program notations in scopes. - Correct priority semantics in typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10759 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04Mise en place d'une extension de apply pour que celui-ci sacheherbelin
traverser les conjonctions (par exemple, apply sur un "iff" cherchera à utiliser la première des 2 composantes qui s'applique). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10758 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04A file that can be loaded when a migration from Set to Type is desiredletouzey
(for instance as a consequence of the Set/Type switch of a library such as FSets). After a "Require Export SetIsType.", Set becomes a mere notation for Type (I love notations !). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10757 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04Correction problème de compil (blast.ml)herbelin
Correction bugs commentaires pour coqdoc (ChoiceFacts.v) Test-suite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10756 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04- Relâchement de la contrainte de bonne longueur des intropatternsherbelin
lorsqu'en position terminale (en fait, l'idéal serait de pouvoir mettre des tactiques dans les branches, style "intros [H ; tac | ]") (cf un exemple QvMake.v) - Pas de delta du tout quand on fait de la recherche de sous-terme (même lorsqu'on vient de apply avec une conclusion ?P t) (cf un exemple dans Rocq/DEMOS/Sorting.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10755 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04Test make 3.81herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10754 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04Quelques améliorations des intro patterns:herbelin
- ajout de -> et <- pour substitution immédiate d'une égalité (comportement à la subst si variable, à la rewrite in * sinon) - ajout possibilité d'hypothèses avec paramètres - correction d'un comportement bizarre de l'utilisation des noms dans cas "[[|] H]" (cf CHANGES) Ce serait bien d'avoir quelque chose comme "intros (H as <-) (H' as [ | ])" pour décider de garder les noms, mais la syntaxe est assez moche. Peut-être un "intros H: <- H': [ | ]" ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10753 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quandherbelin
un lemme avec evars est utilisé localement avec auto ou eauto (clause using). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10752 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04- Amélioration de la présentation de RIneq, même si un nettoyage desherbelin
Hints reste à faire. (dommage que Rge et Rle ne soient pas convertibles) - Ajout de Nnat et Ndigits dans NArith.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10751 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiherbelin
n'était pas encore fait git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10750 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 12:18:08 +0000