aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-02-03maj status de l'extraction des modulesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3649 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-03hack horrible pour renommage dans Modules Types et Functeursletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3648 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-03encore un long_knletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3647 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-02contrib/extraction/table utilise printerletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3646 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-02plus d'environment fixe cur_env mais un environment evolutifletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3645 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-02Bug affichage let destructurantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3644 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-01Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3643 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31Ajout d'un filtrage d'application partielleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3642 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3641 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3640 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3639 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31Unification plus efficace vis à vis du LetInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3638 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31preparation pkg deb for 7.4courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3637 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3636 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31MAJ syntaxe modules + nouveau fichier mod_decl qui explique toutcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3635 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31Pour satisfaire ProofGeneralcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3634 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3633 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Pb de parenthèse dans "Check (S (plus O O))"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3632 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Adds a possibility to construct a term as if it had been parsed throughbertot
a user-defined notation, but without actually using the notation. Changes the files needed to construct the parser : file lib/stamps does not seem to be used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3631 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Make sure the parser is compiled in native mode.bertot
Make sure the coq-interface.opt binary is compiled in native mode (was wrong in the previous version). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3630 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Ajoute les directives pour créer aussi bin/coq-interface.optbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3629 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Auto with zarith essaye Abstract Omega sur un but Falsefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3628 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30changement de place du Initial State (maintenant apres l'analyse de la ligne ↵filliatr
de commande) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3627 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30pas de Xml.vofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3626 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30fignolageletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3625 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30pb d'hier resolu. Recommitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3624 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-29apres le backtrack precedent, remise de trois points precis et sursletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3623 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-29Ca a tout pété -> Bactrack a la version d'hierletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3622 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-29affichage module et module typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3621 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-29affichage module et module typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3620 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-29affichage module et module typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3619 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-28workaround en attendant traitement reel des modules typesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3618 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-28amelioration du pretty-print des modulesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3617 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-28nouvelle gestion des constantes de typeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3616 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-28MAJ pour Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3615 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-27Deux p\'tits trucs ;)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3614 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-25Un type "standardisé" pour new_hypherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3611 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-24on cree toujours le sous-repertoire tactics/filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3609 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-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3606 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-23reparation des contribs: lors de l'unification, reduire les beta redexesbarras
avant d'expanser les constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3604 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-23Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3603 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-23oubli des add_recursors singleton logiquesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3601 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-23status de l'extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3600 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 14:06:18 +0000