aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
| | | | | | | | now. Fix proof scripts that failed correspondingly. Should make many contribs compile again... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 10861Gravatar herbelin2008-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10862 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
| | | | | | | | | | - pour le "try", la nouvelle erreur CannotFindWellTypedAbstraction doit être catchable - pour accomoder Type -1 dans le discharge, il faut un refresh_universes strict - bugs dans les fichiers de test-suite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10861 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
| | | | | | | | | | | | - Un patch pour le bug de non vérification du typage de Stéphane L. - Changement du fameux message "cannot solve a second-order matching problem" en espérant, à défaut de savoir résoudre plus souvent le problème, que le message est plus explicite. - Divers changements cosmétiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
| | | | | | | | | | | | | | | | | | | | | | (i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le principe de la hiérarchie d'univers est d'être cumulative -- et que Set en soit le niveau 0). Une solution aurait été de poser Prop <= Set mais on adopte une autre solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type et Prop <= Set, on garde la représentation de Prop au sein de la hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau sans aucune contrainte inférieure, appelons Type -1) et on adapte les fonctions de sous-typage et de typage pour qu'elle prenne en compte la règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets incidents dans Termops.refresh_universes et Univ.super). Petite uniformisation des noms d'univers et de sortes au passage (univ.ml, univ.mli, term.ml, term.mli et les autres fichiers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite r10857Gravatar herbelin2008-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10858 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report des quelques modifs faites avec Pierre Letouzey sur lesGravatar herbelin2008-04-27
| | | | | | | | fichiers en attendant une intégration à theories/Numbers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10857 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
| | | | | | | | | | | | | | | des types des with-bindings dans la 8.1 [ceux-ci étaient déjà utilisés et ce qui est vraiment nouveau est que l'unification est maintenant celle de evarconv alors que c'était avant un mélange d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je renonce à maintenir la compatibilité (on se retrouve donc avec un exemple qui fonctionne différement dans TermsConv.v de CoLoR). - Robustesse accrue pour la nouvelle facilité de syntaxe de binding avec paramètre pour pose/set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10856 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
| | | | | | | | | | | | | substitution. Makes unification succeed a bit more often, hence auto works better in some cases. - Backtrack the changes of auto using Hint Unfold to do more delta and add a new tactic "new auto" which does that, for compatibility. The first fix may have a big impact on the contribs, whereas the second should make them compile again... we'll see. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10855 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
| | | | | | | | | "pose as" de Program. - Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml. - Comportement de "simple apply" rendu plus proche de celui du apply 8.1 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debug implementation of failing tactics in Morphism to allow earlierGravatar msozeau2008-04-26
| | | | | | | | failures in proof search. Catch Refiner.FailError in typeclasses eauto to indicate that an extern tactic failed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour Gravatar herbelin2008-04-26
| | | | | | | | | | "set (f:=fun n => t)" (et idem pour pose). Documentation notation Record sans sort et, en passant, "let|" -> "let '". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation des fichiers de micromega suite aux changements dansGravatar notin2008-04-25
| | | | | | | | | | setoid_rewrite, et dans Romega. Pour info, ces fichiers ne sont pas compilés... (?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
| | | | | | | | | | | des théorèmes prouvés par récursion ou corécursion mutuelle. Correction au passage du parsing et du printing des tactiques fix/cofix et documentation de ces tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug 1839Gravatar soubiran2008-04-25
| | | | | | | | | | | | | | is line, and those below, will be ignored-- M kernel/mod_subst.mli M kernel/mod_typing.ml M kernel/mod_subst.ml M kernel/subtyping.ml M kernel/modops.ml M library/declaremods.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10849 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix bug in eterm which was not taking filtered contexts in evars intoGravatar msozeau2008-04-25
| | | | | | | | | | account. - Add test case for bug #1844 on Combined Scheme. - Change Reflexive_partial_app_morphism to require a Reflexive proof to cut down search earlier, without losing anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de l'appel à interp_constr pour globaliser une constanteGravatar herbelin2008-04-24
| | | | | | | | | par un appel à global_reference (ce qui évite au passage d'activer le glob dumping). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10845 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1844, generalize implementation to handle and combination ofGravatar msozeau2008-04-24
| | | | | | | Induction and Minimality schemes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10843 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
| | | | | | | | | | | | | | | | debugging and printing hint databases - Typeclasses unfold now correctly adds _global_ unfold hints. - New tactic autosimpl to do simplification using the declared unfold hints in given hint databases. - Work on auto-modulo-some-delta (the declared Unfold constants), actually used mostly if the goal contains evars, as Hint_db.map_auto does not work up-to any conversions (yet). - Fix GenMul which was using the old semantics of failing early because of variance checks, which is not possible in the new implementation. - Restrict when reflexive_morphism may be used using an extern tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840Gravatar herbelin2008-04-24
| | | | | | | | (~/.subversion/config n'avait pas la ligne magique "* = svn:keywords=Author Date Id Revision" dans la section [auto-props]). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | de l'argument donné contient des métavariables (souhait #1408). Beaucoup d'infrastructure autour des constantes pour cela mais qu'on devrait pouvoir récupérer pour analyser plus finement le comportement des constantes en général : 1- Pour insérer les coercions, on utilise une transformation (expérimentale) de Metas vers Evars le temps d'appeler coercion.ml. 2- Pour la compatibilité, on s'interdit d'insérer une coercion entre classes flexibles parce que sinon l'insertion de coercion peut prendre précédence sur la résolution des evars ce qui peut changer les comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN). 3- Pour se souvenir rapidement de la nature flexible ou rigide du symbole de tête d'une constante vis à vis de l'évaluation, on met en place une table associant à chaque constante sa constante de tête (heads.ml) 4- Comme la table des constantes de tête a besoin de connaître l'opacité des variables de section, la partie tables de declare.ml va dans un nouveau decls.ml. Au passage, simplification de coercion.ml, correction de petits bugs (l'interface de Gset.fold n'était pas assez générale; specialize cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml]; whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml]) et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml, classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction d'un bug sur la compostion des substitutions induites par les ↵Gravatar soubiran2008-04-23
| | | | | | alias de module et l'application d'un foncteur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10838 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction du bug sur Parameter Inline que j'ai reouvert hier par inadvertanceGravatar soubiran2008-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added frozen state after each command.Gravatar courtieu2008-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10836 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on change of flags for elim, otherwise rewrite goes underGravatar msozeau2008-04-23
| | | | | | | local variables... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10835 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change default eauto depth to 100 in setoid_rewrite, bump necessaryGravatar msozeau2008-04-23
| | | | | | | | | after introduction of the MorphismProxy indirection. Do local delta conversion in elim. Update CHANGES regarding level of ==> notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10834 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, ↵Gravatar notin2008-04-22
| | | | | | ergo, etc. (cf bug #1831) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10832 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug 1839Gravatar soubiran2008-04-22
| | | | | | | | | | | | -is line, and those below, will be ignored-- M kernel/mod_typing.ml M kernel/subtyping.ml M kernel/modops.ml M library/declaremods.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10829 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed universes bug related to module inclusionGravatar barras2008-04-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10828 85f007b7-540e-0410-9357-904b9bb8a0f7
* test module include w.r.t. universe constraintsGravatar barras2008-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10827 85f007b7-540e-0410-9357-904b9bb8a0f7
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10826 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correct unification for the rewrite variant of setoid_rewrite,Gravatar msozeau2008-04-21
| | | | | | | | so that the example of bug #1425 is accepted. - Backtrack level of notations for morphism signatures to 55. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10825 85f007b7-540e-0410-9357-904b9bb8a0f7
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 12:42:56 +0000