aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Collapse)Author
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-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-08-30Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Serverherbelin
et Set Whelp Getter pour changer le nom des serveurs (report 10105 de la 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10106 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-24Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et ↵herbelin
-rectypes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10091 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-24Utilisation plus précise de la contrainte de type pour interpréter lesherbelin
points-fixes: on applique maintenant cette contrainte avant de généraliser corps et types vis à vis du context (utile notamment en présence de let-in dont on ne sait pas sinon s'ils font partie de la contrainte de type ou du contexte de typage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10088 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-20Modification de l'initialisation des chemins de la librairie standardnotin
pour imposer un ordre précis des répertoires (résout en partie le problème entre Init.Wf et Program.Wf.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10081 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. When the system accepts a fixpoint, it now prints which decreasing argument was used, e.g: plus is recursively defined (decreasing on 1st argument) The search is quite brute-force, and may need to be optimized for huge mutual fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback. N.B. in the standard library, only 4 functions have an decreasing argument different from the one that would be automatically infered: List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind And compiling with as few explicit struct as possible would add about 15s in compilation time for the whole standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-30- Ajout de la possibilité d'utiliser la notation Record pour lesherbelin
coinductifs à un constructeur (suggestion de Georges). - Si pas de sorte ou arité mentionnée dans Inductive/CoInductive/Record, Type est utilisé comme défaut. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9917 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 09:32:09 +0000