aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Collapse)Author
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
(cas d'un terme sans Rel libre), introduction au passage d'un nouveau type d'evar EvarGoal pour raffinement du message d'erreur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
métas permettant de savoir si une instance de méta vient d'un with-binding ou d'une unification, et si elle a déjà été typée ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9866 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-25Modification of VernacScheme to handle a new scheme: Equality (equality invsiles
boolean, will be added later) and update so everything is fine with the new syntax. New Type: type scheme = | InductionScheme of bool * lreference * sort_expr | EqualityScheme of lreference ... | VernacScheme of (lident * scheme) list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-17Nettoyage et standardisation des messages d'erreurs.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
discussion avec Georges) - La notion d'insertion maximale n'est plus globale mais attachée à chaque implicite - Correction de petits bugs dans le calcul des implicites - Raffinement de la notion "sous contexte" pour l'affichage des coercions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-29Multiples changements autour des implicites :herbelin
- correction du mode strict qui n'était pas si strict, - option "Set Strong Strict Implicit" pour activer le mode strictement strict (désactivé par défaut pour raison de compatibilité), - option "Set Reversible Pattern Implicit" pour activer les implicites inférables par unification-pattern (désactivé par défaut par compatibilité), - option "Unset Printing Implicit Defensive" pour désactiver l'affichage des implicites n'ayant pas été décelés stricts, - option "Set Maximal Implicit Insertion" pour que les applications soient saturées en implicites si possible, - une optimisation du mode non strict pour que l'algo de recherche des implicites renonce à calculer les occurrences non strictes qui pourraient avoir à être affichées dans le mode défensif, avec pour conséquence que le mode défensif, pour celui qui le veut, devient a priori encore plus verbeux, ex: Set Implicit Arguments. Definition id x : nat := x. Parameter f : forall n, id n = id n -> Prop. Check (f (refl_equal O)). (* Affichait: "f (refl_equal 0)" mais affiche maintenant "f (n:=0) (refl_equal 0)" *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9812 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-29Correction bug #1507 (report révision 9807 de v8.1 vers trunk)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9809 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-17Reorder hook and printing of message, more natural this way.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9782 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-17 Added the option to set/unset the automatic generation of elimination schemesvsiles
Set Elimination Schemes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9780 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-28Support for implicit formal argument types in Program ; parse types in type ↵msozeau
scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9734 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an ↵msozeau
obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-15Prévention notations récursives sans terminal à gauche et qui font bouclerherbelin
le parser git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9706 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-09bug#1434 importing fonctor arguments, now it works.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9693 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par ↵herbelin
compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles + messages divers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-24Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9678 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-24Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9677 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-21Utilisation de l'environnement pour l'affichage de certains messages d'erreursherbelin
+ petit nettoyage himsg.ml + petite uniformisation erreurs CannotUnify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9668 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-07Vérification que toutes les evars ont étés instanciées dans les types ↵herbelin
implicites des Fixpoint/CoFixpoint (report revision 9617 de 8.1 vers trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9618 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-24Tentative amélioration messages d'erreur prédicat d'élimination (cf notammentherbelin
rapport de bug #1225 -- qui reste ouvert sur le fond) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9527 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-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
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-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-12Correction du bug #1273, deuxième version (avec des shémas d'elimination ↵notin
plus simples) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08Suite ajout option -output-contextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9416 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-08Ajout d'une option -output-context qui affiche le contexte en CCI pur à laherbelin
sortie de session (nécessite option -batch) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9414 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-24Fixed the -emacs option which was always On.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9402 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-21Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deherbelin
chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9398 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-17The emacs-U option now does not output *any* char above 250.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9384 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-02gestion speciale du niveau 5 des ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9333 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
(suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Documentation de "Set Printing Universes", "Print Universes" (anciennementherbelin
"Dump Universes"), "Universe inconsistency", et description brève des univers algébriques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9306 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Ajout option Set Printing Universes et amélioration affichage des universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9304 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23bug #1194: normalisation evars a la sortie de focusbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9261 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23Add a flush after backtracking x y z and before printing subgoals.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9259 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-20Correction de la localisation des erreurs en interactif (numéro deherbelin
ligne relatif à la ligne au lieu de absolu par rapport à la session) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9252 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-09Amélioration de l'automatisation des coupures quand deux idents se suiventherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9227 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ↵notin
d'un constr c, on vérifie que c est clos dans l'environnement de m (#1183) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9217 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-29Added a new option -emacs-U changing emacs prompt delimiters bycourtieu
xml-like patterns (<prompt></prompt>). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9191 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-25Corrections mineuresnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9176 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-20Declarative Proof Language: main commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-15Compatibilité hyp=var dans Tactic Notation + nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9147 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-15Report de l'heuristique d'unification premier ordre flexible/rigideherbelin
en dernière étape de la procédure d'unification - Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution de l'unification premier ordre flexible/rigide - Déplacement check_evars dans Evarutil Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ? (cf exemples d'application dans test-suite/success/evars.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9141 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-12Indentation + svnpropnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9133 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-09Retour à un warning en cas de (co-)fixpoint pas totalement mutuelherbelin
(après tout, d'autres exemples de non totalement mutuels sont acceptés sans problème par la test de bonne fondation - cf add1/add2 dans Sophia-Antipolis/MATHS/GROUPS/Z et Sophia-Antipolis/HARDWARE) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9128 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-06Finalement, interdiction des points fixes non totalement mutuellementherbelin
récursifs parce ce que la condition de garde élimine les appels récursifs sur des sous-termes qui, par construction des types inductifs, ne peuvent ultimement retomber sur un objet du type initial de l'argument de décroissance (p.ex. un appel récursif sur p:positive provenant d'un filtrage sur un z:Z ne sera d'emblée pas considérer sous-terme car la destruction d'un positive ne donnera jamais un Z -- cf exemple de addZ dans une version d'avant aujourd'hui de Sophia-Antipolis/MATHS/GROUPS/Z/Zadd.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9126 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Ajout possibilité clause "where" dans co-points fixes herbelin
(+ uniformisation position notation dans les blocs inductifs et récursifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 07:28:39 +0000