aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2008-04-03Essai d'un peu plus de conversion dans apply : suppression de laherbelin
restriction de conversion sur les sous-termes seulement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10749 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03New file FMapFullAVL containing the balancing proofs about FMapAVL:letouzey
As for FSetAVL vs. FSetFullAVL, preservation of the balancing of trees is not necessary anymore for just fulfilling the Map interface. But we still want theses proofs to exists somewhere, since they ensure the correct efficiency of the FMapAVL operations. In addition, FSetFullAVL also contains the non-structural, ocaml-faithful version of compare. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10748 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03Correction bug 1818, 3eme commentaire. mauvaise generation de substitution a ↵soubiran
l'application du foncteur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10747 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03- Correction d'un bug de coq_makefile sur les variables CAMLLIBS etnotin
COQLIBS. - Ajout d'un message d'erreur si Camlp5 est compilé en mode strict git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10746 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03Rework of FMapAVL inspired by recent changes of FSetAVL: letouzey
* pure functions comes first, proofs are isolated in a sub-module * lazy (&&&) = if ... then ... else true instead of strict (&&) = andb * equal and compare done via continuations * a more clever map2_opt suggested by B. Gregoire: no more intermediate conversion to lists, some sub-functions can handle trivial situations, etc. * map2 is now done via map2_opt and another new iterator: map_option. By the way, this map_option allows to define easily an efficient filter function. Both map2_opt and map_option are currently not available through FMapInterface.S, but they can be used by direct reference to the underlying Raw module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10745 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03Chgts mineurs:herbelin
- correction commit incorrect d'une modif de test-suite/success/apply.v - réorganisation dev/ - renommage Print Modules en Print Libraries - $Id:$ dans g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10744 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03Patch sur le typage d'un foncteur applique a un alias.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10743 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-02Minor fixes. Use expanded type in class_tactics for Morphism search, tomsozeau
alleviate some problems with delta. Better precedence in lambda notation. Temporarily deactivate notations for relation conjunction, equivalence and so on, while we search for a better syntax and maybe a generalization (fixes bug #1820). Better destruct_call in Program.Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10742 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-02Add the ability to specify the implicit status of section variables andmsozeau
whether or not to keep them regardless of the actual dependencies (in order to implement the proper discharge behavior for type classes). This means adding an argument to rebuild_function in libobject, giving this information on variables after a section's constants have been discharged (discharge_function is too early). Surface syntax for Variable not added yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10741 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Typo affichage "simple apply"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10740 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Ajout "simple apply" et "simple eapply" pour apply sans unfoldherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10738 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Finish enhancemenent of return clause inference from tycons, integratingmsozeau
the previous trick of prepare_predicate_from_tycon: if a matched term is dependent, does not appear in the tycon but one of its real arguments is a variable which appears in the tycon, we can transport this dependency in the predicate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10737 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Enhance handling of parameters in typeclass constraints: permit to specify ↵msozeau
any typeclass parameter by name anywhere in a typeclass constraint. This allows to share implementations easily and to give any subset of the parameters in any order in the constraints, whereas we are still restricted to a prefix of the typeclass parameters context when using "positional" specifications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10736 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Add option to set the opacity of obligations to transparent, to be ablemsozeau
to reduce proofs (requested by users). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10735 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Correction du bug #1819notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10734 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-31- Fix for rewriting under dependent products.msozeau
- Use support for abbreviations with params added by Hugo for inverse. - Standard priorities for operators on relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10733 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-30Suite commit 10730: MAJ xlate.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10732 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-30Modifications diverses et variées :herbelin
- Nouvel essai de prise en compte unfold dans apply (unification.ml) - Correction bug commit précédent (constrintern.ml) - Correction bug d'explication des evars non résolues (evarutil.ml) - Fenêtre de query coqide plus large (command_windows.ml) - Orthographe tauto (tauto.ml4) - Crédits (ConstructiveEpsilon.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10731 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
Example: "Notation reflexive R := (forall x, R x x)." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-29Fix test-suite files, change conflicting notation "->rel" and the othersmsozeau
to "-R>" and the like. Split more precisely in inference of case predicate between the new code which currently works only for matched variables and the old one which works better on variables appearing in matched terms types (the two could also be merged). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10729 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-28Improve error handling and messages for typeclasses. msozeau
Add definitions of relational algebra in Classes/RelationClasses including equivalence, inclusion, conjunction and disjunction. Add PartialOrder class and show that we have a partial order on relations. Change SubRelation to subrelation for consistency with the standard library. The caracterization of PartialOrder is a bit original: we require an equivalence and a preorder so that the equivalence relation is equivalent to the conjunction of the order relation and its inverse. We can derive antisymmetry and appropriate morphism instances from this. Also add a fully general heterogeneous definition of respectful from which we can build the non-dependent respectful combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10728 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
[in I] := t [return pred] in b", just as SSReflect does with let:. Change implementation: no longer a separate AST node, just add a case_style annotation on Cases to indicate it (if ML was dependently typed we could ensure that LetPatternStyle Cases have only one term to be matched and one branch, alas...). This factors out most code and we lose no functionality (win ! win !). Add LetPat.v test suite. - Slight improvement of inference of return clauses for dependent pattern matching. If matching a variable of non-dependent type under a tycon that mentions it while giving no return clause, the dependency will be automatically infered. Examples at the end of DepPat. Should get rid of most explicit returns under tycons. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 04:34:56 +0000