aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* ajouts divers pour module PrinterGravatar filliatr1999-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@145 85f007b7-540e-0410-9357-904b9bb8a0f7
* module PrinterGravatar filliatr1999-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@144 85f007b7-540e-0410-9357-904b9bb8a0f7
* module EsyntaxGravatar filliatr1999-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@143 85f007b7-540e-0410-9357-904b9bb8a0f7
* module ExtendGravatar filliatr1999-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@142 85f007b7-540e-0410-9357-904b9bb8a0f7
* typage des existentielles dans Typing_ev; suppression metamap inutiles dans ↵Gravatar filliatr1999-11-25
| | | | | | typage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Des progres dans l'integrationGravatar herbelin1999-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@140 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur modif Evd.evd_conclGravatar herbelin1999-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@139 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
* Version initialeGravatar herbelin1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@137 85f007b7-540e-0410-9357-904b9bb8a0f7
* Versions initialesGravatar herbelin1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplace dans parsingGravatar herbelin1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Version initialeGravatar herbelin1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernacinterp et Vernacentries (partiellement)Gravatar filliatr1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@132 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@131 85f007b7-540e-0410-9357-904b9bb8a0f7
* module WcclausenvGravatar filliatr1999-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@130 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Tactics (debut)Gravatar filliatr1999-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@129 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Tactics (debut)Gravatar filliatr1999-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@128 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Indrec, Wcclausenv; progression dans TacticalsGravatar filliatr1999-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@127 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Pattern, Wcclausenv (interface) et TacticalsGravatar filliatr1999-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@126 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Bij, Gmapl, StockGravatar filliatr1999-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Version préliminaireGravatar herbelin1999-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@124 85f007b7-540e-0410-9357-904b9bb8a0f7
* discriminations netsGravatar filliatr1999-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@123 85f007b7-540e-0410-9357-904b9bb8a0f7
* introduction de Gset et Gmap pour Tlm puis DnGravatar filliatr1999-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@122 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sets et Maps avec egalite generiqueGravatar filliatr1999-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@121 85f007b7-540e-0410-9357-904b9bb8a0f7
* pas de grosse banniere; pas de double point-virgukeGravatar filliatr1999-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@120 85f007b7-540e-0410-9357-904b9bb8a0f7
* On se fait la main: plus de precision si ill-formed rec bodyGravatar herbelin1999-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traducteur ast -> rawtermGravatar herbelin1999-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Type ML des termes non prétypésGravatar herbelin1999-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@117 85f007b7-540e-0410-9357-904b9bb8a0f7
* - répertoire tactics/Gravatar filliatr1999-10-22
| | | | | | | - discrimination nets (début) : modules Tlm et Dn git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@116 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Macros et TacinterpGravatar filliatr1999-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@115 85f007b7-540e-0410-9357-904b9bb8a0f7
* - module Redinfo dans library/ pour les constantes d'éliminationGravatar filliatr1999-10-22
| | | | | | | - module Tacred : fonctions de reductions utilisees dans les tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@114 85f007b7-540e-0410-9357-904b9bb8a0f7
* - documentation repertoire proofs/Gravatar filliatr1999-10-20
| | | | | | | | - IsAppL of constr * constr list ==> répercussion - module Clenv (suite; as terminé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@113 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation proofsGravatar filliatr1999-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@112 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Clenv (debut)Gravatar filliatr1999-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@111 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Evar_refiner et Typing_evGravatar filliatr1999-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@110 85f007b7-540e-0410-9357-904b9bb8a0f7
* module RefinerGravatar filliatr1999-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@109 85f007b7-540e-0410-9357-904b9bb8a0f7
* les variables existentielles contiennent maintenant un environnement (typeGravatar filliatr1999-10-19
| | | | | | | | unsafe_env) et non pas seulement une signature. Le module Evd vient donc apres le module Environ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@108 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place module RefinerGravatar filliatr1999-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@107 85f007b7-540e-0410-9357-904b9bb8a0f7
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
| | | | | | | | | | toujours dans le noyau (en ce sens que Reduction et Typeops les connaissent) mais dans un argument supplémentaire A COTE de l'environnement (de type unsafe_env) - Indtypes et Typing n'utilisent strictement que Evd.empty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@106 85f007b7-540e-0410-9357-904b9bb8a0f7
* module LogicGravatar filliatr1999-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@105 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Proof_treesGravatar filliatr1999-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@104 85f007b7-540e-0410-9357-904b9bb8a0f7
* pas de merge univers dans Declare, car deja fait dans EnvironGravatar filliatr1999-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@103 85f007b7-540e-0410-9357-904b9bb8a0f7
* organisation de trad (entre parsing/ et pretyping/)Gravatar filliatr1999-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@102 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr1999-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@101 85f007b7-540e-0410-9357-904b9bb8a0f7
* plus de recettes pour les corps des constantesGravatar filliatr1999-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@100 85f007b7-540e-0410-9357-904b9bb8a0f7
* - re-introduction d'une evar_map dans unsafe_envGravatar filliatr1999-10-13
| | | | | | | - les var. ex. sont des entiers, et non plus des section_path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@99 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentationGravatar filliatr1999-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@98 85f007b7-540e-0410-9357-904b9bb8a0f7
* redeplacement des var. ex. dans kernel :-)Gravatar filliatr1999-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@97 85f007b7-540e-0410-9357-904b9bb8a0f7
* module LogicGravatar filliatr1999-10-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@96 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 15:14:15 +0000