aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Collapse)Author
2005-12-27Autres suppressions de composantes du traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7744 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-24Changement de stratégie vis à vis du positionnement du module Top en mode ↵herbelin
batch: si rien à compiler, on ouvre Top par défaut, pour l'éviter, il faut l'option -notop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7721 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-23Simplifification de vernac_expr li l'abandon du traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-23Correction printer des Tactic Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7709 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22option '-top dir' now works also in batch mode (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7702 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22option '-top dir' now works also in batch mode; it is even necessary to ↵herbelin
ensure that loaded vernac definitions are defined inside a module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7700 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22Double bug de interp_modifiers anciennement caché par un troisième que les ↵herbelin
nouveaux warnings de ocaml 3.09 avaient révélé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7696 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Divers; restructuration des points d'entrée de Constrinternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7684 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-20Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans ↵herbelin
metasyntax.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7677 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-19Suppression de la mise en boite automatique si format utilisateurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7670 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵herbelin
(suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7662 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵herbelin
et suite correction bug #1028 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-17Orthographe de 'instantiate'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7659 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-23bug de coqide sous windows (bad file descriptor)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7603 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-23bug #909: Top n'est cree que si le contexte est videbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7602 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08- debugging og "Show Intros": no line breaking + fresh idscoq
- added the command "Show Match t" which prints a typical "match...with" for type t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7532 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-04Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7503 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26No parentheses around f in 'f \subst{...}'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7083 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Utilisation du module Buffer; encodage plus rigoureux des symboles en uriherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7082 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Patch to avoid Whelp bug removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7079 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Interface vers outil de recherche Whelpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7049 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵herbelin
aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-15Globalisation des Tactic Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-20Implementation of a new backtracking system, that allow to go backcoq
anywhere in a script (provided no suspend/resume is used): * the command "Backtrack n m p" (vernac_bactrack) performs the following operation: ** do abort p times, ** do undo on the current proof (after the aborts) in order to reach a stack depth of m (see vernac_undo_todepth) ** resets the global state to state labelled with n. * The coq prompt in emacs mode has more informations, it contains: ** the usual coq prompt plus: ** the state number (global state label) ** the depth of the current proof stack ** the names of all pending proofs, in *unspecified* order, separated by '|' Example: state proof stack num depth __ _ aux < 12 |aux|SmallStepAntiReflexive| 4 < ù ^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^ usual pending proofs usual special char git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6947 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-11Ajout récursif du répertoire COQLIB/user-contrib au chemin de chargementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6823 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-01Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6787 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-20Keep ClosedSection marker for resetherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6758 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6750 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6749 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + simplifications and uniformisations + Renaming Print Canonical Structure into Print Canonical Projections git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6744 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + exporting whether a projection is a true projection or a constant associated to a let in the type of the record constructor (fix a bug for canonical structures with let's) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6743 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Ajout Print Canonical Structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-06Nettoyage et documentation de Libraryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Ajout de la syntaxe du reset label: "BackTo n".coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6590 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Affichage numéro de l'état de la commande courante pour mode emacsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6588 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-06- Module/Declare Module syntax made more uniform:sacerdot
* "Module X [binders] [:T] [:= b]." is now used to define a module both in module definitions and module type definitions. Moreover "b" can now be a functor application in every situation (this was not accepted for module definitions in module type definitions) * "Declare Module X : T." is now used to declare a module both in module definitions and module type definitions. - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-03HUGE COMMITsacerdot
1. when applying a functor F(X) := B to a module M, the obtained module is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the body of t in M}. In principle it is now easy to fine tune the behaviour to choose whether b or M.t must be used. This change implies modifications both inside and outside the kernel. 2. for each object in the library it is now necessary to define the behaviour w.r.t. the substitution {X.t := b}. Notice that in many many cases the pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken (in the sense that it used to break several invariants). This commit fixes the behaviours for most of the objects, excluded a) coercions: a future commit should allow any term to be declared as a coercion; moreover the invariant that just a coercion path exists between two classes will be broken by the instantiation. b) global references when used as arguments of a few tactics/commands In all the other cases the behaviour implemented is the one that looks to me as the one expected by the user (if possible): [ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ] a) argument scopes: not expanded b) SYNTAXCONSTANT: expanded c) implicit arguments: not expanded d) coercions: expansion to be done (for now not expanded) e) concrete syntax tree for patterns: expanded f) concrete syntax tree for raw terms: expanded g) evaluable references (used by unfold, delta expansion, etc.): not expanded h) auto's hints: expanded when possible (i.e. when the expansion of the head of the pattern is rigid) i) realizers (for program extraction): nothing is done since the actual code does not look for the realizer of definitions with a body; however this solution is fragile. l) syntax and notation: expanded m) structures and canonical structures: an invariant says that no parameter can happear in them ==> the substitution always yelds the original term n) stuff related to V7 syntax: since this part of the code is doomed to disappear, I have made no effort to fix a reasonable semantics; not expanded is the default one applied o) RefArgTypes: to be understood. For now a warning is issued whether expanded != not expanded, and the not expanded solution is chosen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵herbelin
printers dans ocamldebug; partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6550 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵herbelin
printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant ↵herbelin
dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-25 09:27:25 +0000