aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
| | | | | | | | | | | | | | | | term unification (for constant and variable delta unfolding) and one to parameterize closed-term conversion. Most of the time conversion uses full delta and unification does no delta. This fine-grain is used in rewrite/setoid_rewrite, where only closed-term delta on global constants is allowed. - Interpret Hint Unfold as a directive for delta conversion in auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints). - Remove ad-hoc support for this in typeclasses. Now setoid_rewrite works correctly w.r.t. the old version regarding local definitions. - Fix closed bugs which needed updating due to syntax modifications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10824 85f007b7-540e-0410-9357-904b9bb8a0f7
* Addded the "Dump Tree" command.Gravatar cek2008-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10823 85f007b7-540e-0410-9357-904b9bb8a0f7
* corection bug #1837Gravatar soubiran2008-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10822 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1838 + doc modules.Gravatar soubiran2008-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
| | | | | | | | | | lists of occurrences through tactics. Implement the "at" variants of setoid_replace correspondingly. Fix in class_tactics efor w_unify not checking types when unifying a meta with anything (problematic at top-level only). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the ability to give a transparent_state for conversion, toGravatar msozeau2008-04-20
| | | | | | | | parameterize what should be unfolded or not, by default unfolding everything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10819 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test pour compilation native camlp5Gravatar herbelin2008-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10818 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour engendrer version.tex, adoption de printf qui, au contraire deGravatar herbelin2008-04-18
| | | | | | | | echo, devrait marcher pareil sous Ubuntu comme sous les autres systèmes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1835 + correction bug occur-check résultant en unGravatar herbelin2008-04-18
| | | | | | | | | | | | "cannot define an evar twice" --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M tacred.ml M evarutil.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10815 85f007b7-540e-0410-9357-904b9bb8a0f7
* pbm avec echoGravatar filliatr2008-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10814 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug squashing day !Gravatar msozeau2008-04-17
| | | | | | | | | | | | | | | | | - Closed bugs 121, 1696, 1438, 1425, 1696, 1604, 1738, 1760, 1683 related to setoids. Add corresponding test files. - Add new modulo_zeta flag to control zeta during unification (e.g. not allowed for setoid_rewrite unification, but ok for almost everything else). - Various fixes in class_tactics with respect to evars and error messages. - Correct error message for NoOccurenceFound, distinguishing between a rewrite in the goal or an hypothesis. - Move notations for ==>, --> and ++> to level 90 as suggested by Russell O'Conor. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10813 85f007b7-540e-0410-9357-904b9bb8a0f7
* No compatibility notations for andb and co (this restore a correct Print output)Gravatar letouzey2008-04-17
| | | | | | | | | | | | The benefit of these "only-parsing" notations in Bool.v were to avoid replacing qualified Bool.andb by Datatypes.andb and so on. But such Bool.xxxx are fairly rare (e.g. none in contribs), and these notations have one serious drawback: with them, Print andb leads to Datatypes.andb instead of the body of andb. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prevent the apparition of &&& when printing a (if ... then ... else false)Gravatar letouzey2008-04-17
| | | | | | | | and idem for |||, thanks to a specific scope lazy_bool_scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10811 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactique gappaGravatar filliatr2008-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10810 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation tactique gappaGravatar filliatr2008-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add almost empty Classes.tex for documentation of type classes.Gravatar msozeau2008-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10808 85f007b7-540e-0410-9357-904b9bb8a0f7
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
| | | | | | | | | | | | | | | - More meaningful argument name for resolve_typeclasses. - Try to remove unneeded instance declarations in Morphisms. - Allow the proofs of reflexivity arising from unchanged arguments in setoid_rewrite to be fullfiled by Morphism instances and not necessariy because the relation is reflexive (needed by higher-order morphisms). Use a new "MorphismProxy" class to implement that efficiently. - Fix a bug in abstract_generalize not delta-reducing a type where it should. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)Gravatar letouzey2008-04-16
| | | | | | | | | | 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
* first-order --> firstorder (kills a warning about not being a valid id)Gravatar letouzey2008-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10805 85f007b7-540e-0410-9357-904b9bb8a0f7
* flottantsGravatar filliatr2008-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a function that escapes XML characters in ppcmds.Gravatar cek2008-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10803 85f007b7-540e-0410-9357-904b9bb8a0f7
* More renamings to avoid clashes (e.g. with CoRN).Gravatar msozeau2008-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mises à jour bugs, CHANGES, code mortGravatar herbelin2008-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
| | | | | | | | 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
* * added a subsection to explain the automatic declaration of schemes:Gravatar vsiles2008-04-15
| | | | | | | | | | | | | | * 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
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
| | | | | | | | | | | | 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
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
| | | | | | | | | | | | | | | | - 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
* typoGravatar vsiles2008-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10795 85f007b7-540e-0410-9357-904b9bb8a0f7
* fix some bogus calls to id_of_string by the extractionGravatar letouzey2008-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10794 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinPos: New version of ~1 and ~0 notations, xH replaced by 1 and proofs cleanupGravatar letouzey2008-04-14
| | | | | | | | | 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
* oubli sur 10790Gravatar herbelin2008-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10792 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite 10790 (identificateurs)Gravatar herbelin2008-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10791 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses corrections Gravatar herbelin2008-04-14
| | | | | | | | | | | | | | - 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
* Update doc and remove another overloading of equiv_*.Gravatar msozeau2008-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renamings to avoid clashes with definitions in Relation_Definitions, nowGravatar msozeau2008-04-14
| | | | | | | | | 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
* Fix setoid tests, use red for a Setoid_Theory lemma, and ParametricGravatar msozeau2008-04-14
| | | | | | | Relation for function spaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
| | | | | | | | | | | | | | | | | | | | | | - 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
* Désactivation du dumping des notations quand funind appelle lesGravatar herbelin2008-04-12
| | | | | | | | commandes d'interprétation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document the new setoid rewrite tactic, and fix a few things whileGravatar msozeau2008-04-12
| | | | | | | | | | | | 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
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
| | | | | | | | | | | | 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
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
| | | | | | | | | | | 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
* Check that no evars remain in instance types earlier at InstanceGravatar msozeau2008-04-11
| | | | | | | declarations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10779 85f007b7-540e-0410-9357-904b9bb8a0f7
* Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicitGravatar msozeau2008-04-09
| | | | | | | 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
* Verify Setoid is loaded before doing anything.Gravatar msozeau2008-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in new Morphisms files. Gravatar msozeau2008-04-09
| | | | | | | | | | | | | | - 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
* Fix evar bugs in type classes:Gravatar msozeau2008-04-09
| | | | | | | | | | - 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
* contradict can now handle False hypothesis in the spirit of contradictionGravatar letouzey2008-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug List.map2 dans Case12.vGravatar herbelin2008-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10770 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the last compilation problemGravatar msozeau2008-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10769 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation problemGravatar msozeau2008-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10768 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-19 14:16:02 +0000