aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-07-26- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avecherbelin
paramètres - ce qui satisfait la requête #1899 - et only parsing), en attendant l'avis de Pierre. - Des "points finals" manquants dans himsg.ml (cf 11230). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11268 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-25Suite 11266 (warning tools/gallina.ml)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11267 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-25Correction d'une incohérence de typage des inductifs polymorphes: lesherbelin
contraintes bornant par le haut le type de l'inductif (ce qui peut arriver quand l'inductif est argument d'une constante) étaient oubliées : on pouvait se retrouver avec des inductifs dont le type des constructeurs, une fois instancié par des paramètres) n'était plus typable (seul leur réduit, après expansion des constantes, était typable). [kernel, test-suite] + Affichage des inductifs (via Print) en prenant la forme utilisateur des constructeurs. + Correction warning dans compilation gallina.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-25Fixed bug #1904 (instances of evars were no longer substituted sinceherbelin
the context of fixpoint was typechecked binder per binder and not as whole) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11265 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-25A better test for relations being setoids or not: do leibniz rewrite iffmsozeau
the applied relation is an abbreviation for @eq. Fixes bug #1915. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11264 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-25More compatibility fixes, revert the tauto fix that preventedmsozeau
destruction of records as a lot of scripts currently rely on it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11263 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24Tauto breaking not only binary "conjunctions" seems like a bad ideamsozeau
after all... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11259 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24A (safe) implementation of prolog's cut in the typeclasses eauto to avoidmsozeau
redoing proofs for nothing, i.e, do not backtrack on proofs whose evars are disjoint from the evars of the rest of the goals. Fixes the example in bug #1911, needs some more testing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11258 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24Fix bug #1913, checking for unresolved evars which aren't obligations.msozeau
Also check mutuality of fixpoints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11257 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24fixed loop in dependency fold of the checkerbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11256 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24moved magic numbers to configure (share coq/coqchk)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11254 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24broke cyclic dependenciesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11253 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24Suite commit 11236notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11252 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24Propagation de l'information "strict" (càd à toplevel ou en train deherbelin
définir une ltac) dans l'interprétation des identificateurs isolés en position de tactiques, comme dans "let x:=y in t" (résoud l'incompatibilité #1906). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11250 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-23Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theherbelin
opportunity to extend the class of singleton types to (possibly mutual) recursive types with single constructors of which all arguments are in Prop. This covers Acc. Acc_rect can consequently be defined in the direct way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11249 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-23Stop glob messages to be printed by default on stdout letouzey
Jean-Marc, feel free to check I've not broken anything concerning coqdoc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11248 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-23Oops... forgot some debug code.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11247 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22Add test-suite file for bug# 1905 and minor fix in Program/Equality.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11245 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22New tactics [conv] to test convertibility (actually, unification) of twomsozeau
terms and [head_of_constr id] to put the head of a constr in some new hypothesis. Both are used in a new tactic to deal with partial applications in setoid_rewrite. Also fix bug #1905 by using [subrelation] to take care of [Morphism (R ==> R') id] constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11244 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22A try at allowing matching on applications as a binary syntax node by default.msozeau
It breaks tauto as [?X _ _] matches much more terms. It is mostly fixed by not destructing objects of record types. The new [intuition] was also pulling an unneeded dependency in Field_theory which can be cleared easily. Zis_gcd_bezout is also considered a conjunction now, which seems correct(?). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11243 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
setting "Set Manual Implicit Arguments" for manual-only implicits. Fix test-suite script. This removes the discharge_info argument of "dynamic" object's rebuild function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11242 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22Oubli lors du commit #11236notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11241 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-21Suite commit 11236notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11240 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-20Extraction: better dependency computation (after optimisations)letouzey
When doing monolithic extraction, the initial dependency graph may turn to be too broad thanks to later optimisations. We now do an extra dependency pass at the end, killing more useless code. In addition, when doing an "Extract Constant t => ...", if t isn't an axiom, we don't include the dependencies of the body of t. This may break earlier extraction setups (with or without Extract Constant), since they may take advantage of objects that were earlier "wrongly" included in the extracted code. The fix is simple : just add these missing objects to the extraction command-line. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11239 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18- Rebranchement backtrack du langage déclaratif dans Coqideherbelin
- Divers: message d'erreur et typo relatifs au langage déclaratif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11237 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵notin
de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18Modification rapide du message d'erreur lorsqu'un _ ne peut êtreherbelin
effacé dans un intro-pattern (suggéré par ssreflect). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11235 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18Affichage intempestif d'information de globalisation + numéro de version ↵notin
dans coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11234 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-17fixed indentation of subgoals for Show Scriptbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11233 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-17- Suppression de Rstar/Newman peu utilisables comme biblio (encodageherbelin
des inductifs à l'ordre supérieur par exemple) et qui sont de toutes façons accessible en contrib dans Rocq/CoC_History. - MAJ numéro de version dans Tutorial.tex git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11232 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-17- coqdoc: correction d'un bug sur les commentaires imbriquésnotin
- coq_makefile: amélioration des chemins de camlp4/5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11231 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-16Ajout de cibles pour le manuel de référence (refman-nodep, stdlib-nodep, ↵notin
refman-quick) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11229 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-16ROmega : make it work even if no Require Import ZArith has been doneletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11228 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-16Ajout d'une option pour contrôler l'installation automatique de la ↵notin
documentation + ajout d'un test pour hevea et latex git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11227 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-16Quelques modifications autour du filtrage Ltac:herbelin
- Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas où c'est le n-ième sous-termes qui finalement réussit (passage à une complexité en n plutôt que n^2, via l'utilisation de continuations). - Sémantique du filtrage: suppression dans sub_match de la recherche dans le type des let (puisque ce n'est pas cencé être une information utilisateur) mais rajout de la recherche dans le champ cast qui lui est utilisateur. - Nouvelle fonctionnalité: récupération des noms des variables liantes filtrées (dans matches/sub_match) et utilisation de ces noms dans ltac (utile pour récupérer x dans "exists x, P x"); git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11226 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-15Autour du parsing:herbelin
- Utilisation de notations de type "abbreviation paramétrée" plutôt que de notations introduisant des mots-clés, là où c'est possible (cela affecte QDen, in_left/in_right, inhabited, S/P dans NZCyclic). - Extension du lexeur pour qu'il prenne le plus long token valide au lieu d'échouer sur un plus long préfixe non valide de token (permet notamment de faire passer la notation de Georges "'C_ G ( A )" sans invalider toute séquence commençant par 'C et non suivie de _) - Rajout d'un point final à certains messages d'erreur qui n'en avaient pas. - Ajout String.copy dans string_of_label ("trou" de mutabilité signalé par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui ouvert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-15Tentative de relecture des scripts de Mult.v au regard des tactiques actuellesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11224 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-13update doc Micromegafbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11223 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-11Correction d'un autre bug autour de la gestion des niveaux vides deherbelin
camlp4 (faire l'initialisation dans l'ordre: les sous-niveaux vides, eux-mêmes dans l'ordre, avant de créer le niveau de la notation elle-même). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11220 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-10Bug résiduel du backtrack de coqide se produisant lorsque la limite deherbelin
la pile de undo de tactique est atteinte (il ne fallait pas oublier de faire un abort). On en profite pour porter cette limite à une valeur significativement plus élevée. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11219 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-09Documentation fixes. msozeau
Thanks to Samuel Bronson for pointing out [Typeclasses unfold] was not referenced from the Setoid doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11217 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-09test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eqletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11216 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-08forgotten debug printf in coqmktop (anyway, can be obtained by -echo)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11215 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-08Suite de la révision #11212notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11214 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-07Fix implicit arguments in sections bug and check for resolution of evars whenmsozeau
defining records. Fix test-suite script because of new implicit argument setting for DefaultRelation. Fix regression in auto, changing the order of tried lemmas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11213 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-07Utilisation de try_locate_qualified_library au lieu de ↵notin
locate_qualified_library (suite commit #11177) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11212 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-07Micromega: doc + test-suite updatefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11211 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-07- Improve [Context] vernacular to allow arbitrary binders, not justmsozeau
classes, and simplify the implementation. - Experimental syntax {{ cl : Class args }} and (( cl : Class args )) which respectively make cl an implicit or explicit argument ({{ }} is equivalent to [ ]). Could be extended to any type of binder, eg. [Definition flip ((R : relation carrier)) : relation carrier := ...]. The idea behind double brackets is to distinguish macro-binders which perform implicit generalization from regular binders. It could also save [ ] for other uses. - Fix bug #1901 about {} binders in records. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11210 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-04Fix bug #1899: no more strange notations for Qge and Qgtletouzey
In fact, Qge and Ggt disappear, and we only leave notations for > and >= that map directly to Qlt and Qle. We also adopt the same approach for BigN, BigZ, BigQ. By the way, various clean-up concerning Zeq_bool, Zle_bool and similar functions for Q. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11205 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 18:59:56 +0000