aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2007-01-22Correction pour le rapport de bug #1325 par rétablissement duherbelin
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
2007-01-22Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouentherbelin
(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
2007-01-19Prise en compte des univers algébriques dans les types inférés dansherbelin
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
2007-01-19Export de l'afficheur de substitutions de noms de modules pour le débogueurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9504 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-19Protection contre les warnings 'unused variable' de ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9503 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-19Protection contre les warnings 'unused variable' de ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9502 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-19Tests de référence circulaire au sous-typage de module (pour mémoire)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9501 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-18Update installation instructions to the modern world a bit.lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9500 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-18Update for v8.1lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9499 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17Move definition of VO_TOOLS_DEP before first use of it.lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9498 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17Reintroduce compatibility with old versions of GNU makelmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9497 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17Correction bug #1282herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9495 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17Correction bug #1302herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9494 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17Correction adresse CoRN dans FAQ (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9492 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17Correction adresse CoRN dans FAQ (cf #1317)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9491 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17README update:lmamane
- 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
2007-01-15Various subtac fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9485 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-12Suite au mail de Lionel a propos du Makefile: letouzey
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
2007-01-12un saut de ligne ...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9483 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-12addition du neq unicodeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9482 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-11Petit oubli dans commit 9474herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9480 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-11Ajout d'une option de débogage pour expliciter l'instance des evarsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9479 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-10 - Make .vo files depend on coqdoc if COQ_XML is set (bug #848)lmamane
- 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
2007-01-10Merge with Lionel Elie Mamane's private branch:lmamane
- 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
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
- 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
2007-01-10Suite commit restructuration discharge (application du type deherbelin
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
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
- 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
2007-01-08Subtac fixes, support for reasoning on wf defs.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9473 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-05suite de la reparation du bug 1239: apres les inds, les records et vars de typesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9471 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-02Rework subtac pattern matching equalities generation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9470 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-02Add f_equal case for 6 arguments.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9469 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-29Protection contre une source possible de liaison de lambda anonymeherbelin
(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
2006-12-28Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àherbelin
égalité décidable + maj dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-28Correction petits bugs du check de la test-suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9466 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-28Remplacement de la définition de Pind et Prec par une définitionherbelin
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
2006-12-28Cleaning backtracking code, optimized "Backtrack n x y" when n iscourtieu
current state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-26Report correction bug #1289 dans trunk (r9435 pour branche v8.1)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9463 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-23Doc for Combined Scheme.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9462 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-23Addition of a "Combined Scheme" vernacular command for building the ↵msozeau
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
2006-12-22Default tactic for solving goals.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9460 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-22remplacement d'un test d'egalite par un test de convertibilite dans ↵jforest
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
2006-12-21typo malencontreusefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9458 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-19Adaptation à Subversion 1.4notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9457 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-17reparation bug 1239letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9455 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-15contrib/dp: tactique ergo (voir ergo.lri.fr)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9453 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-14Confusion sur le paramètre à donner à concrete_name lors du commit 9450herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9452 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-14Reimplemented equality generation for pattern matching at typing time. First ↵msozeau
version. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9451 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-13Alignement de la politique de renommage de rename_bound_var (utilisé pourherbelin
résoudre la clause with de apply/elim) sur la politique de renommage de concrete_name git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9450 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-13test condition de gardebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9449 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 22:49:00 +0000