aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Pb de parenthèse dans "Check (S (plus O O))"Gravatar herbelin2003-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3632 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a possibility to construct a term as if it had been parsed throughGravatar bertot2003-01-30
| | | | | | | | | | 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
* Make sure the parser is compiled in native mode.Gravatar bertot2003-01-30
| | | | | | | | 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
* Ajoute les directives pour créer aussi bin/coq-interface.optGravatar bertot2003-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3629 85f007b7-540e-0410-9357-904b9bb8a0f7
* Auto with zarith essaye Abstract Omega sur un but FalseGravatar filliatr2003-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3628 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement de place du Initial State (maintenant apres l'analyse de la ligne ↵Gravatar filliatr2003-01-30
| | | | | | de commande) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3627 85f007b7-540e-0410-9357-904b9bb8a0f7
* pas de Xml.voGravatar filliatr2003-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3626 85f007b7-540e-0410-9357-904b9bb8a0f7
* fignolageGravatar letouzey2003-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3625 85f007b7-540e-0410-9357-904b9bb8a0f7
* pb d'hier resolu. RecommitGravatar letouzey2003-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3624 85f007b7-540e-0410-9357-904b9bb8a0f7
* apres le backtrack precedent, remise de trois points precis et sursGravatar letouzey2003-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ca a tout pété -> Bactrack a la version d'hierGravatar letouzey2003-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3622 85f007b7-540e-0410-9357-904b9bb8a0f7
* affichage module et module typeGravatar letouzey2003-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3621 85f007b7-540e-0410-9357-904b9bb8a0f7
* affichage module et module typeGravatar letouzey2003-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3620 85f007b7-540e-0410-9357-904b9bb8a0f7
* affichage module et module typeGravatar letouzey2003-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3619 85f007b7-540e-0410-9357-904b9bb8a0f7
* workaround en attendant traitement reel des modules typesGravatar letouzey2003-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3618 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration du pretty-print des modulesGravatar letouzey2003-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3617 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle gestion des constantes de typeGravatar letouzey2003-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3616 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour RegGravatar desmettr2003-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deux p\'tits trucs ;)Gravatar coq2003-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3614 85f007b7-540e-0410-9357-904b9bb8a0f7
* all tactics should be covered now: remainsGravatar bertot2003-01-26
| | | | | | | 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
* Add translations for many tactics but a dozen are still remainingGravatar bertot2003-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3612 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un type "standardisé" pour new_hypGravatar herbelin2003-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3611 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inspect does not work for pcoq and there is no simple fix because inspectGravatar bertot2003-01-24
| | | | | | | | | 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
* on cree toujours le sous-repertoire tactics/Gravatar filliatr2003-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3609 85f007b7-540e-0410-9357-904b9bb8a0f7
* The data constructed when detecting an error in a list of commands mustGravatar bertot2003-01-24
| | | | | | | 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
* Corrects the way conjunctions, existential quantifications, and arrows areGravatar bertot2003-01-24
| | | | | | | 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
* majGravatar filliatr2003-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make sure proof by pointing works.Gravatar bertot2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3605 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation des contribs: lors de l'unification, reduire les beta redexesGravatar barras2003-01-23
| | | | | | | avant d'expanser les constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).Gravatar corbinea2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make proof by pointing work for the new notations of existential quantification.Gravatar bertot2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3602 85f007b7-540e-0410-9357-904b9bb8a0f7
* oubli des add_recursors singleton logiquesGravatar letouzey2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3601 85f007b7-540e-0410-9357-904b9bb8a0f7
* status de l'extractionGravatar letouzey2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3600 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj V7.4Gravatar letouzey2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3599 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mauvais environnement d'évaluation pour les globauxGravatar herbelin2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3597 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3596 85f007b7-540e-0410-9357-904b9bb8a0f7
* modified the unification algorithm to try first order unification beforeGravatar barras2003-01-22
| | | | | | | doing head beta-reduction. (cf coqbugs #181) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation du contenu de REALSGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3594 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de whd_state dans l'interfaceGravatar barras2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3593 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changements dans REALSGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3592 85f007b7-540e-0410-9357-904b9bb8a0f7
* removes all references to ctast.ml the Makefile has been updated accordingly.Gravatar bertot2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans SeqPropGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans Rtrigo_defGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3589 85f007b7-540e-0410-9357-904b9bb8a0f7
* I changed the interface to make sure SearchAbout is defined according toGravatar bertot2003-01-22
| | | | | | | the same design pattern as the other search commands. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3588 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3587 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages nombreuxGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3586 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3585 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug réecriture à la racine pour le sétoide Prop.Gravatar clrenard2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage f_pos -> IVT (Intermediate Value TheoremGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3583 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-20 23:08:25 +0000