aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Various improvements in handling of evars in general and typingGravatar msozeau2008-06-21
| | | | | | | | | | | | | | | | | | | | | | | constraints in Program: - normalize types and defs of local fixpoints before checking the guardness condition to avoid having to give type annotations, e.g: << Definition fold (A B : Set) (f : B -> A -> B) : B -> tree A -> B := fix aux acc t := match t with | Leaf x => f acc x | Node l => fold_left aux l acc end. >> - add new inh_coerce_to_prod to allow coercion of the typing constraint to a product before trying to split it. It's a noop in standard mode, and forgets subsets in Program. Allows to typecheck: << (λ x, x) : { f : nat -> nat | ... } >>. - Better handling of the "abstract" typing constraints in Program. - Correctly normalize w.r.t. evars. the tycon given by users in Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11156 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo in a commentGravatar letouzey2008-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11155 85f007b7-540e-0410-9357-904b9bb8a0f7
* Little fixes: print unbound variable in error message (patch by SamuelGravatar msozeau2008-06-19
| | | | | | | | Bronson), some keywords in coqdoc, and test well-typedness of predicate in subtac_cases after abstraction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11153 85f007b7-540e-0410-9357-904b9bb8a0f7
* incomplete bugfix for infoGravatar corbinea2008-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11149 85f007b7-540e-0410-9357-904b9bb8a0f7
* removed unwanted linebreaks in pretty printingGravatar corbinea2008-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11148 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
| | | | | | | | (résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in implementation of splitting of class constraints.Gravatar msozeau2008-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in subtac:Gravatar msozeau2008-06-18
| | | | | | | | | | | | - Use return clause inference in addition to the automatic generation of equalities for pattern-matching. - Disallow generation of coercions between type constructors, which are not provable anyway. - Improve inference for local (co-)fixpoints using the typing constraint. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11140 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibility fixes (Add Setoid bug and accidental introduction of aGravatar msozeau2008-06-18
| | | | | | | tactic named "app"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11139 85f007b7-540e-0410-9357-904b9bb8a0f7
* meilleur gestion de la fonction de "cache" des alias (declaremods), et ↵Gravatar soubiran2008-06-18
| | | | | | correction d'un bug sur Import/Export module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11138 85f007b7-540e-0410-9357-904b9bb8a0f7
* Detection de l'architecture sous Windows (et sans uname -o)Gravatar notin2008-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11137 85f007b7-540e-0410-9357-904b9bb8a0f7
* Où l'on se débarrasse de uname -oGravatar notin2008-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in handling of classes and instances inside sections atGravatar msozeau2008-06-17
| | | | | | | discharge time. Also fix bug when loading modules containing classes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup in subtac_cases, preparing to use improvements on return predicateGravatar msozeau2008-06-17
| | | | | | | | | inference. Little improvement un subtac_obligations: do not retry to solve all obligations when finishing to solve one obligation nobody depends on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes w.r.t. let binders in class contexts and Add ParametricGravatar msozeau2008-06-17
| | | | | | | Morphism/Relation bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11132 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better typeclass error messages, always giving the full set ofGravatar msozeau2008-06-17
| | | | | | | | unsatisfiable constraints. Add a resolution call in tacinterp before trying the default tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
| | | | | | | | | | | | | | disambiguate syntax: [ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x : nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will not parse. Add applicative contexts in tactics match, to be able to match arbitrary partial applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end will bind C to [ ∙ 1 2 ] and x to 0. Minor improvements in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
| | | | | | | | | | restriction du contexte était attendue) + suppression warning + amélioration affichage en cas de clause "at" incorrecte + report commit 11121 (correction bug 1367) de la 8.2 vers le trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11128 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: 2 problèmes de undo encore:Gravatar herbelin2008-06-13
| | | | | | | | | | | | - dans le "replay", l'état n'était pas correctement sauvegardé d'où une perte d'efficacité en cas de rejeux répétés, - bug de synchronisation dans le calcul de la pile des lemmes ouverts. + réajout de la variante standard de Set Printing All dans le menu display. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Temporary fix for bug #1876, printing fails because of unresolvedGravatar msozeau2008-06-13
| | | | | | | globals. Change program_simpl to use [auto] and not [auto with *]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numéros de version dans la docGravatar notin2008-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11123 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un problème lié à une interaction entre hyperref etGravatar notin2008-06-12
| | | | | | | | | | | | | latex, qui empechait de produire des fichiers .dvi à partir des .tex générés par coqdoc. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/tools/coqdoc/coqdoc.sty M branches/v8.2/tools/coqdoc/coqdoc.sty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing the definitions of pred and minus in the style of GGGravatar werner2008-06-12
| | | | | | | | in order for them to preserve the structural order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction parser révélé par test-suiteGravatar herbelin2008-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compilation WindowsGravatar notin2008-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des 'cp' et 'mkdir' par 'install'Gravatar notin2008-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Confusion sur commit précédent de library. La capture du Not_foundGravatar herbelin2008-06-12
| | | | | | | | | | dans la recherche du nom long était bien utile (parce que la table des filename n'est plus synchronisée et plus dans le initial.coq) mais c'est ailleurs qu'on reposait à tort sur la bonne synchronisation de la table des noms longs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11111 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans l'adaptation de library_full_filename lors du débranchementGravatar herbelin2008-06-11
| | | | | | | | des filename hors reset (r11077). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug alias d'alias.Gravatar soubiran2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'export des .cmi dans coq_makefileGravatar notin2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optionally (and by default) split typeclasses evars into connected Gravatar msozeau2008-06-11
| | | | | | | | components and resolving them separately, reporting more precise failures. Improve error messages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11105 85f007b7-540e-0410-9357-904b9bb8a0f7
* now Escape toggles query paneGravatar jnarboux2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11103 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ diversesGravatar herbelin2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plutôt que de reposer sur le vernacexpr pour détecter les débuts deGravatar herbelin2008-06-11
| | | | | | | | | | buts, on se base sur les informations de Pfedit (comme le fait Pierre Courtieu). Permet d'être plus robuste sur les extensions de syntaxe ouvrant des buts, style Function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".Gravatar herbelin2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11100 85f007b7-540e-0410-9357-904b9bb8a0f7
* escape key now hides paneGravatar jnarboux2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zpow_facts.Zmult_power: kills a useless hypothesisGravatar letouzey2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout query Locate dans coqide sur suggestion Arthur C.Gravatar herbelin2008-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11097 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.Gravatar herbelin2008-06-10
| | | | | | | - Test match dépendant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11095 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
| | | | | | | | | | | | | | | - Changement au passage de la convention "at -n1 ... -n2" en "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut pas mélanger des positifs et des négatifs. - Au passage: - simplification de gclause avec fusion de onconcl et concl_occs, - généralisation de l'utilisation de la désignation des occurrences par la négative aux cas de setoid_rewrite, clrewrite et rewrite at, - correction d'un bug de "rewrite in at" qui utilisait le at de la conclusion dans les hyps. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7
* open and save buttons are the defaultGravatar barras2008-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11093 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correct handling of DependentMorphism error, using tclFAIL instead ofGravatar msozeau2008-06-10
| | | | | | | | | | | | letting the exception go uncatched. - Reorder definitions in Morphisms, move the PER on (R ==> R') in Morphisms where it can be declared properly. Add an instance for Equivalence => Per. - Change bug#1604 test file to the new semantics of [setoid_rewrite at] - More unicode characters parsed by coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2-3 petites modifs sur la docGravatar notin2008-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur l'"optimisation" de admit (révision 11084). Comme leGravatar herbelin2008-06-10
| | | | | | | | | | | fait remarquer Bruno, c'est ne pas anodin de laisser croire qu'on admet une conjecture alors qu'on admet uniquement la conclusion de cette conjecture, conclusion qui peut être incohérente et qui ne le serait pas si on avait gardé le contexte du but. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11089 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction d'un bug sur la commande Include. Gravatar soubiran2008-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the number parsing/printing for BigN/BigZ/BigQGravatar letouzey2008-06-10
| | | | | | | | | | | | | | | | | | | | | * In order to get via a "SearchAbout bigZ" all the generic lemmas that are now available, I moved bigZ to a notation for BigZ.t instead of a definition. But this notation was interacting badly with the number parsing. * Moreover, I also discovered that printing was broken as well, due to a reference to obsolete name Basic_type (now DoubleType) that I forgot to adapt in g_intsyntax. * Last but not least, there was also a bug not due to myself that was probably preventing parsing/printing _very_ big numbers (the ones for which generic constructor BigN.Nn is used): this Nn is the 7-th constructor, not the 13-th. In addition, the first argument to Nn was supposed to be automatically inferred, this was not working, so we build it now explicitely (very easy). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11087 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de la dépendance de Micromega envers Coq.Reals.Reals. Corrige ↵Gravatar notin2008-06-10
| | | | | | le bug #1867 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11086 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction bug 1841 (identificateurs incorrects avec Subclass)Gravatar herbelin2008-06-10
| | | | | | | | - Correction wish 1866 (un "admit" plus fin dans sa généralisation des hyps) - Bricoles dans cases.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11085 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction de la version simplifiée (filtrage sur deux sigGravatar herbelin2008-06-09
| | | | | | | | | | imbriqués) du bug 1834, mais le bug 1834 reste ouvert [cases.ml]. - Réactivation de l'interprétation des listes dans "generalize" cassée depuis 11072) [tacinterp.ml]. - Bricoles et petit nettoyage en passant [cases.ml et g_vernac.ml4]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un comportement special du sous-typage pour les constantes opaques.Gravatar soubiran2008-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11082 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 17:03:52 +0000