aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2007-10-02Fix a problem doing 'make clean' under Winodwsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10165 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-02Report des modifications faites sur le configure en r10039, r10052, r10053 ↵notin
et r10054 dans les branches trunk et v8.1 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10164 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-02Now NMake is provedthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10163 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-02Correcting error message when adding Setoid, Relation or morphism (bug #1626)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10162 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-01Added the compilation of theories/Numbers to Makefile.common. The following ↵emakarov
things compile: abstract natural numbers and integers with plus, times, minus, and order; Peano and binary implementations for natural numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10161 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-01Nouvelle mise à jourherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10160 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-01Amendement à la révision 10124 : déplacement de apprec_nohdbeta entreherbelin
is_fconv et le test d'équations simples (on admettra que is_fconv est a priori plus efficace pour réduire que nohdbeta -- et de fait, sur Stalmarck/algoRun, apprec_nohdbeta part en vrille alors que if_fconv réussit vite). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10159 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-01Complément nécessaire aux révisions 10156 et 10157herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10158 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-30Suite de 10157herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10157 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-30Ajout infos de débogage de "universe inconsistency" quand option Setherbelin
Printing Universes est active. Ajout de l'option "using" à la tactique non documentée "auto decomp". Ajout de la base "extcore" pour étendre "auto decomp" avec des principes élémentaires tels que le dépliage de "iff". Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28Creation of a new token PATTERNIDENT (?ident) for intro patterns, soglondu
that "intros ? a ? b" behaves as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10155 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28On empêche "fresh" d'engendrer un mot-clé.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10154 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28On Linux, we read /proc/self/exe to get the executable's path insteadglondu
of just relying on $0. This is needed, e.g. when coqtop -byte is being called via a link which is in $PATH, but coqtop.byte is not in $PATH. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10153 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28Correction bug 1711herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10151 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28Oubli dans Setoid.vnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10150 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28 Forget to update the CHANGES filevsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10149 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28Modification of the Scheme command.vsiles
Now you can forget to provide the name of the scheme, it will be built automatically depending of the sorts involved. e.g. Scheme Induction for nat Sort Set. will build nat_rec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10148 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-27Découpage de Setoid.vnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10147 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-27Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0herbelin
(crédits à Sylvie Boldo) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10146 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-26Complément aux commits 10124 et 10125 sur l'inférence de type (correction herbelin
de plusieurs bugs d'indice, de List.rev, d'oubli d'application de whd_evar + code plus concis pour l'argument optionnel "filter"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10145 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-26 added a lemma to prove inj_pair2 when eq_dec is available.vsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10144 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-25An update on theories/Numbers.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10142 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-25Changes in Backtrack documentation. More accurate.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10141 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-25Suppression de tous les alias de la forme x:=x dans la compilation du filtrage.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10140 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-24Added the documentation for Backtrack and BackTo.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10139 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21curpat_ty was in a smaller contextmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10137 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21Petit complément au commit 10131.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10136 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21Correction d'un bug dans check + ajout de testsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10134 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21Update on theories/Numbersemakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10133 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21Update on theories/Numbers. Natural numbers are mostly complete,emakarov
need to make NZOrdAxiomsSig a subtype of NAxiomsSig. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10132 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
the latter is bound to a var which is not a quantified one - this led to remove a line marked "temporary compatibility" ... ; made a distinction between quantified hypothesis as for "intros until" and binding names as in "apply with"; in both cases, we now expect that a identifier not used as a variable, as in "apply f_equal with f:=g" where "f" is a true binder name in f_equal, must not be used as a variable elsewhere [see corresponding change in Ints/Tactic.v]) - Fixing bug 1643 (bug in the algorithm used to possibly reuse a global name in the recursive calls of a coinductive term) - Fixing bug 1699 (bug in contracting nested patterns at printing time when the return clause of the subpatterns is dependent) - Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic) - Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-20Changed the definition of Nminus in BinNat.v by removing comparison.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10130 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-19Indication de quel type de constantes est dépliable dans "simpl" (cfherbelin
message de Benjamin Pierce de sep 2007 sur coq-club) [report de la révision 10128 de la 8.1 vers le trunk] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10129 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-18MAJ date copyright docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10127 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-18Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10125 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-17Raffinement de l'algorithme d'inférence de typeherbelin
----------------------------------------------- - Les fonctions evar_define et real_clean font un travail plus fin : - S'il y a plusieurs manières d'inverser l'instance d'une evar, on retarde le choix au lieu de faire un choix arbitraire. - Si l'instance contient une evar et que cette evar n'est pas inversible, on essaie aussi d'inverser ou de restreindre (un sous-terme) de l'evar qui était initialement à instancier. - Incidemment, real_clean est renommé en invert_instance, un nom qui reflète mieux la diversité du travail fait par ce fameux real_clean. - La fonction solve_refl garde les problèmes qui contiennent encore de l'information. - Changements secondaires : - Délégation de la gestion des variables modifiées et des problèmes à reconsidérer (get_conv_pbs) à Evd (qui s'en charge par effet de bord au moment du define) (incidemment get_conv_pbs devient extract_conv_pbs) - Essai d'un mécanisme différent de restriction des evars : pour éviter des contextes mal formés (comme do_restrict pouvait a priori le faire), on utilise maintenant un contexte bien formé doublé d'un filtre signalant les instances interdites. C'est a priori plus souple (par ex : si une variable du contexte a un type dépendant d'une evar, on peut attendre de connaître cette evar avec de déterminer si cette variable du contexte, qui peut-être dépend via cette evar d'une autre variable interdite, doit être finalement interdite ou pas) - Nettoyages divers. - Ce que evarutil ne fait toujours pas : - Utiliser l'inversion et/ou l'unification d'ordre supérieur (par exemple pour résoudre "?ev[S n]=n"); en particulier, la notion d'inversion unique ne prend pas en compte l'unification d'ordre supérieur et peut donc faire des choix irréversibles vis à vis de l'unif d'ordre supérieur. - Utiliser (systématiquement -- et précautionneusement) les types des solutions trouvées pour résoudre davantage de problèmes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10124 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-16Réponse à une incompatibilité introduite dans 10114 (calcul du nombreherbelin
de solutions distinctes faites modulo égalité d'alias uniquement et pas modulo toute la puissance de la convertibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10123 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-14Correction du bug #1679 (congruence) et ajout test-suitecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10120 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-13Update before joining all signatures into one.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10119 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-07- renaming Qle_shift_recip_r into Qle_shift_inv_r, etcroconnor
- Adding Qlt_shift_div_l, etc - Adding Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b). - Adding Qle_Qabs : forall a, a <= Qabs a. - Removing redudnent Qminus' x y := Qred (Qminus x y) from Qabs. It is already defined elsewhere (in it's proper place). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10118 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-06errors in recdef.ml4:bertot
a few errors of parentheses around fun x -> ... constructs, a use of tclTHEN was left over from bug tracking modifications, it was badly parenthesized. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10117 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-06this should fix a problem described in a message by Dufourd on July 30th, 2007bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10116 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
evdref si evar_defs ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-06Itération sur les sous-termes dans la vérification de la condition de gardeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10114 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-04fixed iconsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10113 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-04fixed iconsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10112 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-04Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte lesherbelin
alias de variables dans la fonction d'inversion des instance (real_clean): - détection des cas d'inversions distinctes incompatibles - nouvelle heuristique lorsque plusieurs inversions distinctes mais compatibles existent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10111 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-01A word on the measure and wf modifiersmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10110 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-01Suite commit 10103 (expansion des défs locales triviales dans l'étapeherbelin
de "projection" lors de l'instanciation d'une evar -- fonction "real_clean") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10109 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 14:15:07 +0000