aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Suppression d'un Import R_scope probablement oublieGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3582 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans RListGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3580 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour renommage RcompletGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans RcompleteGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage Rcomplet.v -> Rcomplete.vGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de lemmes superflusGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3576 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans PartSumGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 'with Module' corrigeGravatar coq2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3573 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug precedenceGravatar herbelin2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3572 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit bug pp haskellGravatar letouzey2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3571 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction des modules, enfin !Gravatar letouzey2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3569 85f007b7-540e-0410-9357-904b9bb8a0f7
* id_of_msid en plusGravatar letouzey2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3568 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation à la nouvelle sémantique plus uniforme de "Match term"Gravatar herbelin2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3567 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueurGravatar herbelin2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3566 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 11:50:19 +0000