aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* Add -browser option to configure scriptGravatar glondu2008-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11271 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
| | | | | | | | | | | 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
* - Suppression de Rstar/Newman peu utilisables comme biblio (encodageGravatar herbelin2008-07-17
| | | | | | | | | | 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
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
| | | | | | | | | | | | | | | | | - 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
* Documentation Prop<=Set et Arguments Scope GlobalGravatar herbelin2008-07-01
| | | | | | | Correction au passage d'un bug de Arguments Scope Global git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
| | | | | | | | | | | | | | | | | - Option -R fait maintenant des Import à tous les niveaux de la hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche. - Option -I rend maintenant possible l'accès aux sous-répertoires via les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il rend récursivement visibles les noms non qualifiés. - Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir. - Ajout option -exclude-dir pour exclure certains sous-répertoires de la descente récursive de -R. - Amélioration message de localisation pour fichiers venant d'un "state". - Adaptation du checker (et ajout du test check_coq_overwriting qui semblait involontairement oublié dans l'option -R). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ fichiers spécifiques trunkGravatar herbelin2008-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11164 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | discriminate/injection/simplify_eq acceptent maintenant un terme comme argument. Les clauses "with" et les variantes "e" sont aussi acceptées. Aussi, discriminate sans argument essaie maintenant toutes les hyps quantifiées (au lieu de traiter seulement les buts t1<>t2). --This line, and those below, will be ignored-- M doc/refman/RefMan-tac.tex M CHANGES M pretyping/evd.ml M pretyping/termops.ml M pretyping/termops.mli M pretyping/clenv.ml M tactics/extratactics.ml4 M tactics/inv.ml M tactics/equality.ml M tactics/tactics.mli M tactics/equality.mli M tactics/tacticals.ml M tactics/eqdecide.ml4 M tactics/tacinterp.ml M tactics/tactics.ml M tactics/extratactics.mli M toplevel/auto_ind_decl.ml M contrib/funind/invfun.ml M test-suite/success/Discriminate.v M test-suite/success/Injection.v M proofs/clenvtac.mli M proofs/clenvtac.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 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
* Documentation de "instantiate".Gravatar glondu2008-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11080 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation de admit et Print Assumptions.Gravatar herbelin2008-06-09
| | | | | | | | | | | | - Relecture, mise à jour, correction d'erreurs et petite réorganisation du chapitre sur les commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers algébriques). - Suppression de la dépendance du initial.coq en les noms longs des fichiers de façons à ce que les dépendances ne soient que purement logique. - Encore un (petit) bug undo ide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
| | | | | | | | | - MAJ CHANGES et COMPATIBILITY - Réservation de || et && dans Notations.v - code mort et MAJ suite commit 11072 (tactics.ml et changes.txt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11073 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
| | | | | | | | | | | | | | | | | - Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
* add tiny change to coqideGravatar jnarboux2008-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11066 85f007b7-540e-0410-9357-904b9bb8a0f7
* One (last?) more update of CHANGES.Gravatar letouzey2008-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11056 85f007b7-540e-0410-9357-904b9bb8a0f7
* more updates of CHANGESGravatar letouzey2008-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some updates of CHANGES (to be continued...)Gravatar letouzey2008-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11043 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inGravatar letouzey2008-06-01
| | | | | | | | a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t))) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"Gravatar herbelin2008-05-30
| | | | | | | | | | n'étaient pas gérés, merci à Julien). - Correction pb blocage CoqIDE quand le browser n'est pas déja lancé (utilisation pour cela de Sys.command au lieu de Unix.open_process_full). - MAJ CHANGES et COMPATIBILITY. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11022 85f007b7-540e-0410-9357-904b9bb8a0f7
* update changes related to coqideGravatar jnarboux2008-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10998 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Nouvelle option "Set Printing Existential Instances" pour forcerGravatar herbelin2008-05-25
| | | | | | | | | | l'affichage des instances des evars. - Nouveaux boutons "interrupteurs" pour activer/désactiver à volonté l'affichage des implicites, coercions, notations, etc dans CoqIDE (reste à trouver des icônes appropriées !). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la possibilité d'utiliser fix/cofix dans les notations.Gravatar herbelin2008-05-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10981 85f007b7-540e-0410-9357-904b9bb8a0f7
* refined the conversion oracleGravatar barras2008-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Léger backtrack sur commit coqide précédent (si la commande à annulerGravatar herbelin2008-05-20
| | | | | | | | | à potentiellement modifié l'état, on ne peut se contenter d'un Abort : il faut revenir au dernier état connu). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10951 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix bug related to indices of fixpoints.Gravatar msozeau2008-05-13
| | | | | | | | | | | - Add a typeclasses_eauto which uses only the typeclass_instances database. - Set obligations as transparent by default to avoid the common problem with ill-formed recursive defs due to opaque obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10925 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ et bricoles diversesGravatar herbelin2008-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10923 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
| | | | | | | | | | | | | | binders. - Change syntax of type class instances to better match the usual syntax of lemmas/definitions with name first, then arguments ":" instance. Update theories/Classes accordingly. - Correct globalization of tactic references when doing Ltac :=/::=, update documentation. - Remove the not so useful "(x &)" and "{{x}}" syntaxes from Program.Utils, and subset_scope as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]Gravatar herbelin2008-05-09
| | | | | | | pour les listes (trop contraignant) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | du filtrage. Cela permet de détecter les cas impossibles et de simuler les contraintes d'inversion exprimables sous la forme d'un assignement des arguments du constructeurs (cf le cas de Vtail dans Bvector.v). Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi) avec vi composé uniquement de constructeurs, et que le résultat final est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on construit le prédicat Q:=fun x1 .. xn y => match x1 .. xn y with | v1(z) .. vn(z) t => P(z) | _ .. _ _ => ?evar-speciale-cas-impossible end qui vérifiera bien que Q u1 .. un = P(w1,..,wp). En raison de limitations de l'unification (on aurait besoin d'eta conversion pour résoudre des problèmes du genre "terme rigide == match x with _ => ?evar end", et besoin d'instanciation par constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"), je n'ai pas réussi à traiter le cas général. Aussi, on adopte une stratégie pragmatique consistant à tester plusieurs prédicats possibles : - si un type final est donné, on essaie d'abord l'algorithme de Matthieu et sinon le nouvel algorithme (permet par exemple de traiter certains cas d'élimination dépendante de Bvector.v), - s'il n'y a pas de type final, on essaie d'abord le nouvel algo et sinon, on essaie avec un prédicat sans dépendance (permet de traiter des cas compliqués comme celui de par cas sur I' dans le fichier Case13.v de la test-suite). Dans la pratique, il y a beaucoup de changement dans le code de compile_case. - Par exemple, la compilation est maintenant toujours appelé avec un prédicat (là où l'on pouvait avoir None, on a maintenant toujours au moins une evar). - En revanche, le membre droit des clauses est maintenant optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une branche impossible au moment du calcul du prédicat de retour. - Aussi, on renonce aux PrLetIn et PrProd dans l'expression du predicat de retour mais il faut savoir que c'est maintenant la liste des tomatchs qui spécifie le contexte exact dans lequel le prédicat de retour est bien typé. - Et d'autres... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 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
* 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
* - 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
* - 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
* 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
* 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
* 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
* 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
* Mises à jour bugs, CHANGES, code mortGravatar herbelin2008-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
| | | | | | | | SetoidTactics and document it. Cleanup Classes.Equivalence. Minor fixes to the Program doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10799 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
| | | | | | | | | | | | | | | | - Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
| | | | | | | | | | | | | | | | | | | | | | - vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite 10760Gravatar herbelin2008-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'une extension de apply pour que celui-ci sacheGravatar herbelin2008-04-04
| | | | | | | | traverser les conjonctions (par exemple, apply sur un "iff" cherchera à utiliser la première des 2 composantes qui s'applique). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
| | | | | | | | | | | | | | | | | | - ajout de -> et <- pour substitution immédiate d'une égalité (comportement à la subst si variable, à la rewrite in * sinon) - ajout possibilité d'hypothèses avec paramètres - correction d'un comportement bizarre de l'utilisation des noms dans cas "[[|] H]" (cf CHANGES) Ce serait bien d'avoir quelque chose comme "intros (H as <-) (H' as [ | ])" pour décider de garder les noms, mais la syntaxe est assez moche. Peut-être un "intros H: <- H': [ | ]" ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
| | | | | | | | Example: "Notation reflexive R := (forall x, R x x)." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interpret patterns for hypotheses types in match goal in type_scope (if not aGravatar msozeau2008-03-25
| | | | | | | | context [] pattern). May break some user contribs... Rename clsubstitute to substitute. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur les réels:Gravatar herbelin2008-03-23
| | | | | | | | | | | | | | | | | | | | | | | | - Renommage de Rlt_not_le de Fourier_util en Rlt_not_le_frac_opp pour éviter la confusion avec le Rlt_not_le de RIneq. - Quelques variantes de lemmes en plus dans RIneq. - Déplacement des énoncés de sigT dans sig (y compris la complétude) et utilisation de la notation { l:R | }. - Suppression hypothèse inutile de ln_exists1. - Ajout notation ² pour Rsqr. Au passage: - Déplacement de dec_inh_nat_subset_has_unique_least_element de ChoiceFacts vers Wf_nat. - Correction de l'espace en trop dans les notations de Specif.v liées à "&". - MAJ fichier CHANGES Note: il reste un axiome dans Ranalysis (raison technique: Ltac ne sait pas manipuler un terme ouvert) et dans Rtrigo.v ("sin PI/2 = 1" non prouvé). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10710 85f007b7-540e-0410-9357-904b9bb8a0f7
* migration of the old IntMap library from StdLib to a user contrib ↵Gravatar letouzey2008-03-19
| | | | | | (Cachan/IntMap) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10699 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 00:50:47 +0000