aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Factorize code for internalization of binders to fix bug #1846. AlsoGravatar msozeau2008-05-04
| | | | | | | | | rewrite interp_context to use this new code instead of doing internalization by itself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques éléments de réflexionGravatar herbelin2008-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
| | | | | | | | in a separate function in Refiner and use it in eauto to capture the same semantics as auto (which uses tclTRY) when trying tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10879 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
| | | | | | | | | | | particulier, TacCall(_,f,[]) est utilisé pour une référence à une variable ltac ou une tactique et Reference(f) est utilisé pour une référence à une variable ltac ou un constr (en passant, standardisation de l'utilisation de constr: ou ltac: à setoid_ring). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10878 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
| | | | | | | | | | constantes qui avait été mise en place pour la 8.1gamma puis abandonné pour cause entre autres d'inefficacité. Cette fois, on restreind le polymorphisme au seul cas d'alias vers un inductif. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contournement laborieux de la "feature" de camlp5 qui entrainait leGravatar herbelin2008-04-30
| | | | | | | | | | | bug "no level labelled 8" (camlp5 ne sait pas annuler un extend lorsque le niveau initial existe mais est vide : l'appel à delete efface le niveau au lieu d'annuler l'effet de extend et de revenir à un niveau existant vide). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct a bug in "new auto" and also unify_eqn which did not do localGravatar msozeau2008-04-30
| | | | | | | | delta conversion when it should (setoid_rewrite bug reported by roconnor). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Calcul plus robuste du numéro de révision (ne marche en positionnantGravatar herbelin2008-04-29
| | | | | | | | | | | LANG que si LC_ALL n'est pas lui-même défini) --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M Makefile.build git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
| | | | | | | | | | | syntaxe interne de ring_lookup et field_lookup qui n'était pas assez robuste pour supporter une syntaxe [ ... ] dans constr. Déplacement de now_show de List.v vers Tactics.v, déplacement de "[ _ ]" au niveau 0. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de la partie ML de la contrib correctness. Les fichiersGravatar herbelin2008-04-29
| | | | | | | | | n'étaient plus compilés depuis le 14 janvier 2004 (avant la 8.0), Why ayant pris la suite de correctness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans coq_makefile: génération des règles implicites ↵Gravatar notin2008-04-29
| | | | | | en présence de l'option -custom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix eauto still using delta when it shouldn't (should make CoRN compileGravatar msozeau2008-04-29
| | | | | | | | | | in reasonable time), add (unfinished) documentation on type classes. Put some classes into Prop explicitely as singleton inductive types are no longer in Prop by default even if all the arguments are (is that really what we want? roconnor says no). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10868 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation bug de compil introduit au precedent commitGravatar jforest2008-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10866 85f007b7-540e-0410-9357-904b9bb8a0f7
* menage dans funind + deplaceemnt de recdef dans funindGravatar jforest2008-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10865 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 07:22:46 +0000