aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
AgeCommit message (Collapse)Author
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-10Remove a TODO in the translation of generic arguments:bertot
the case of casted open constr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3751 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-06Make sure that identifiers are parsed as qualified identifier and thatbertot
the whole text is considered, not only the prefix that can be considered as an identifier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3745 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-05Ajout du traducteurdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-03Added a clause for VernacDefineModule, but with an error as result.bertot
This is more work to do to have a complete treatement of the Vernac syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3651 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-26all tactics should be covered now: remainsbertot
TacAlias, but does not seem to be active code for now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3613 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-25Add translations for many tactics but a dozen are still remainingbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3612 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-24Inspect does not work for pcoq and there is no simple fix because inspectbertot
has not be put among the hooks in the pcoq_hook structure. As a temporary solution, we use a replacement command named "Pcoq_inspect" that behaves like Inspect 15. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3610 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-24The data constructed when detecting an error in a list of commands mustbertot
imperatively be called PARSING_ERROR and not PARSE_ERROR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3608 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-24Corrects the way conjunctions, existential quantifications, and arrows arebertot
treated in eliminations for proof-by-pointing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3607 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-23Make sure proof by pointing works.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3605 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-23Make proof by pointing work for the new notations of existential quantification.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3602 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22removes all references to ctast.ml the Makefile has been updated accordingly.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3591 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Make sure pcoq will also display hypotheses with a value.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3553 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Add a few operators in the new version of xlate.ml and make surebertot
that ast_to_ct is not use anymore in translate_constr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3552 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵herbelin
la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3533 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵herbelin
une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3497 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-06SearchAboutfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3489 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19simplification de solve_subgoal: n'utilise plus frontierbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3458 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Ajout "Locate Notation"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3442 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-12Ajout du vernac Proof withgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3418 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Ajoute le bon traitement pour Ring, Locate, Commentsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3404 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Take notations into account: numbers and the CNotation operator.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3401 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-04Modification Require Frommohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3376 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-03la table PARAMETER n'existe plus (mergé dans la table CONSTANT)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3369 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-03Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvellesbertot
syntaxes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3362 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29Raffinement syntaxe Infixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3344 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵herbelin
améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-16Complétion du commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3247 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-15Passage à une représentation des fixpoints plus primitive dans constr_expr ↵herbelin
(càd avec indices) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3245 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur ↵herbelin
affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3185 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Clarification changements autour de Remark/Fact/Localherbelin
Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3180 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-14TacCall attend une référenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3142 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-14Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneherbelin
référence donnée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3133 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ↵herbelin
hack temporaire autour du printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3120 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07Lazy manuelles dans le codecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-06correcting the treatment of many tactics that use quant_hyp in file xlate.mlbertot
and associated file. Also adding a systematic check approach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3092 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-04Re-introduce the treatement of Tacticals that Hugo had already done inbertot
a previous mail. Correct a problem in the handling of out_gen for Inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3087 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-03Previous version did compile but did not make it possible to actually runbertot
pcoq. This version does work. Main modification is: - change centaur.ml4 so that * the Pcoq mode is really started by Start Pcoq Mode. * Reset <id> and Reset Initial work as planned for Pcoq (commands are Pcoq Reset <id> and Pcoq ResetInitial). * current_proof_name() does not raise an exception when there is no current proof. - change xlate.ml so that the main tacticals are translated correctly to pcoq data structures. - change in ascent.mli so that * we make sure Fail can now have a numeric argument, * progress is added - vtp.ml is changed in accordance with ascent.mli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3078 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Complétion filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3046 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3031 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pourherbelin
les définitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2852 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; ↵herbelin
rparation de la protection contre les clauses indiscernables de TACTIC EXTEND et VERNAC COMMAND EXTEND; rparation des grammaires de Extraction, EAuto, TextMode, KillProof et Derive Dependent Inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2753 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Intgration uniforme de coercions dans les dclarations (Variable and co) et ↵herbelin
retouche des Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2747 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 09:27:31 +0000