aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Derivation of (exists x : A, P x) -> {x : A | P x} for decidable PGravatar emakarov2007-01-23
| | | | | | | | and countable A. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9522 85f007b7-540e-0410-9357-904b9bb8a0f7
* ring : Correction du bug PR#1306Gravatar bgregoir2007-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9520 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1315:Gravatar notin2007-01-22
| | | | | | | | | | | | | | | | | | - ajouts des opérations clear_evar_hyps_in_evar, clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui permettent de supprimer des hypothèses dans le contexte des evars, en créant une nouvelle evar avec un contexte restreint; - adaptation de clear_hyps dans Logic pour qu'elle mette à jour le contexte des evars; - adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié; - déplacement de la tactique Change_evars dans prim_rule. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug d'unification-pattern dans l'algo d'unificationGravatar herbelin2007-01-22
| | | | | | | | des tactiques (ne marchait que si l'instance était une application). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9516 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allègement de l'affichage des références par le printer si possibleGravatar herbelin2007-01-22
| | | | | | | | | | | | (on garde des noms de la forme IND(name,i) et CONSTR(name,i,j) que lorsqu'on ne sait pas le bon nom, i.e. pour les IND mutuels autres que le premier et pour tous les constructeurs). Pour un affichage complètement explicite des noms avec ocamldebug, charger maintenant set_raw_db en plus de db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification redondance Axiome du choix unique/descriptionGravatar herbelin2007-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9513 85f007b7-540e-0410-9357-904b9bb8a0f7
* changes in declarative language : by term using tacticGravatar corbinea2007-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9512 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour le rapport de bug #1325 par rétablissement duGravatar herbelin2007-01-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | comportement pré-inductifs polymorphes vis à vis du test d'inclusion des hypothèses de section (i.e. test dans le noyau mais pas dans typing.ml qui est le typeur utilisé généralement par les tactiques). En effet, les variables de section sont vues par les tactiques comme des variables locales qui sont modifiables (p.ex. par conversion). Mais le changement de la signature des variables de section fait échouer le typage noyau (qui exige une égalité syntaxique des types de ces variables) pour les demandes de typage en provenance des tactiques. Quelle est la bonne solution ? - Faut-il comparer les variables de section modulo réduction dans le noyau ? - Faut-il continuer à utiliser un typeur qui ne teste pas les hyps de section pour les tactiques, comme c'était le cas avant les inductifs polymorphes (c'est la solution pragmatique adoptée pour résoudre #1325) - Faut-il éviter la confusion entre variables de section et variables de but ? Incidemment, branchement de Tacmach.hnf_type_of sur Retyping, ce qui, outre des calculs de typage allégés pour les tactiques, évite aussi de tomber sur le comportement du bug #1325. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9510 85f007b7-540e-0410-9357-904b9bb8a0f7
* Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouentGravatar herbelin2007-01-22
| | | | | | | (particulièrement intéressant pour simplify du fait de sa proximité avec simpl) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9508 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des univers algébriques dans les types inférés dansGravatar herbelin2007-01-19
| | | | | | | | | les interfaces de module (bug similaire à #1302 mais pour les définitions -- au lieu des inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de l'afficheur de substitutions de noms de modules pour le débogueurGravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9504 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9503 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les warnings 'unused variable' de ocaml 3.09Gravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tests de référence circulaire au sous-typage de module (pour mémoire)Gravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9501 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update installation instructions to the modern world a bit.Gravatar lmamane2007-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update for v8.1Gravatar lmamane2007-01-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9499 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move definition of VO_TOOLS_DEP before first use of it.Gravatar lmamane2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9498 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reintroduce compatibility with old versions of GNU makeGravatar lmamane2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1282Gravatar herbelin2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9495 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1302Gravatar herbelin2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9494 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction adresse CoRN dans FAQ (suite)Gravatar herbelin2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction adresse CoRN dans FAQ (cf #1317)Gravatar herbelin2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9491 85f007b7-540e-0410-9357-904b9bb8a0f7
* README update:Gravatar lmamane2007-01-17
| | | | | | | | | | - GNU Make version 3.80 or later is needed. - a C compiler is needed. - not all ./configure options are listed, refer people to "./configure -help". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various subtac fixes.Gravatar msozeau2007-01-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite au mail de Lionel a propos du Makefile: Gravatar letouzey2007-01-12
| | | | | | | | | | | | | | | | | 1) Disparition de test_extraction.v rebasculé dans test-suite/success/extraction.v Au passage, remplacement de quelques Set en Type pour ne pas avoir besoin du -impredicative-set. Et ajout de passes d'extraction en Haskell et Scheme. Simplification du Makefile en conséquence (plus de barestate) 2) Au passage, reparation (et embellissement) de extract_env. Depuis le passage de Claudio dans cette portion (il y a 2 ans ?), faire Extraction S (ou tout autre constructeur) echouait. Idem pour un nom d'inductif mutuel autre que le premier du paquet. Etonnant que personne n'ait remarqué ca plus tot... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9484 85f007b7-540e-0410-9357-904b9bb8a0f7
* un saut de ligne ...Gravatar letouzey2007-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9483 85f007b7-540e-0410-9357-904b9bb8a0f7
* addition du neq unicodeGravatar letouzey2007-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit oubli dans commit 9474Gravatar herbelin2007-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9480 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option de débogage pour expliciter l'instance des evarsGravatar herbelin2007-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9479 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Make .vo files depend on coqdoc if COQ_XML is set (bug #848)Gravatar lmamane2007-01-10
| | | | | | | | - Clean up NO_RECOMPILE_LIB treatment a bit - Clean up .vo dependencies in general git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge with Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
| | | | | | | | - Fix previous merge (semantic/type conflict in code added minutes before my commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9477 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - Makefile: Option (environment variable NO_RECOMPILE_LIB) to not recompile the whole standard library just because the coq binaries got rebuilt. - Infrastructure to change the object pretty-printers at runtime. - Use that infrastructure to make coqtop-protocol with Pcoq trees and Pcoq-protocol with pretty-printed terms possible in coq-interface. - Make "Back(track)" into closed sections, modules and module types "Just Work™". - Modernise/generalise Pcoq protocol a bit, make some of its warts optional. - Implement "Show." in Pcoq mode. - Add Rpow_def.vo to REALSBASEVO so that its dependencies are computed (and used). - "make revision" now handles GNU Arch / tla in addition to svn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit restructuration discharge (application du type deGravatar herbelin2007-01-10
| | | | | | | discharge_function des implicites au cas des scopes d'arguments) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Avant : une unique méthode discharge_function qui avait accès à l'ancien environnement mais pas de possibilité de raisonner avec les objets du nouvel environnement en cours de construction. C'était problématique pour le discharge des implicites, arguments scope, etc qui étaient finalement faits en même temps que le discharge des constantes et inductifs mais avec pour effets de bord que les entrées dans la lib_stk arrivaient juste avant celles des constantes et inductifs avec des problèmes pour effacer les bonnes entrées au moment du reset - Maintenant : deux méthodes distinctes : discharge_function qui est appliquée pour collecter de l'ancien environnement ce qui est à garder dans la section et rebuild_function qui reconstruit le nouvel environnement connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant l'extensibilité que la méthode ancienne du fichier discharge.ml ne permettait pas) Au passage, ajout d'un modificateur Global aux déclarations d'implicites et d'arguments scopes pour indiquer qu'elles doivent perdurer à la sortie de la section Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps discharged reste) Au passage, nettoyage impargs.ml, suppression code mort résiduel du traducteur etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac fixes, support for reasoning on wf defs.Gravatar msozeau2007-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9473 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite de la reparation du bug 1239: apres les inds, les records et vars de typesGravatar letouzey2007-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rework subtac pattern matching equalities generation.Gravatar msozeau2007-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add f_equal case for 6 arguments.Gravatar msozeau2007-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre une source possible de liaison de lambda anonymeGravatar herbelin2006-12-29
| | | | | | | (utilisation du nom de la contrainte de type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àGravatar herbelin2006-12-28
| | | | | | | égalité décidable + maj dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction petits bugs du check de la test-suiteGravatar herbelin2006-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9466 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de la définition de Pind et Prec par une définitionGravatar herbelin2006-12-28
| | | | | | | | | suggérée par Conor McBride qui ne fait pas intervenir eq_rect et qui permet de montrer "facilement" (mais avec l'axiome K) les équations de réduction de Prec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9465 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning backtracking code, optimized "Backtrack n x y" when n isGravatar courtieu2006-12-28
| | | | | | current state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report correction bug #1289 dans trunk (r9435 pour branche v8.1)Gravatar herbelin2006-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Doc for Combined Scheme.Gravatar msozeau2006-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Addition of a "Combined Scheme" vernacular command for building the ↵Gravatar msozeau2006-12-23
| | | | | | | | | conjunction of mutual inductions principles. e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9461 85f007b7-540e-0410-9357-904b9bb8a0f7
* Default tactic for solving goals.Gravatar msozeau2006-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9460 85f007b7-540e-0410-9357-904b9bb8a0f7
* remplacement d'un test d'egalite par un test de convertibilite dans ↵Gravatar jforest2006-12-22
| | | | | | injection/discriminate/inversion pour corriger des bugs en presence de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9459 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo malencontreuseGravatar filliatr2006-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation à Subversion 1.4Gravatar notin2006-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9457 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 00:20:01 +0000