aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Collapse)AuthorAge
* ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de ↵Gravatar letouzey2002-01-18
| | | | | | contrib/omega vers theories/ZArith git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2406 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrthographeGravatar herbelin2002-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2392 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj CHANGES extraction + bug extraction & _Gravatar letouzey2001-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2359 85f007b7-540e-0410-9357-904b9bb8a0f7
* contrib/interface/dad.ml4 had no real need of streams, it should have beenGravatar bertot2001-12-19
| | | | | | | | translated into a regular ml files like the others. This mistake is now corrected. The Makefile and dependency files are updated accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2345 85f007b7-540e-0410-9357-904b9bb8a0f7
* debranchement du test sur les RealsGravatar letouzey2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2344 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation du make depend et du .dependGravatar letouzey2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrections post contournement des streams avec ++Gravatar herbelin2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2332 85f007b7-540e-0410-9357-904b9bb8a0f7
* the function Ctast.section_path was wrong. It performed two reverseGravatar bertot2001-12-18
| | | | | | | operations on lists, which was equivalent to doing nothing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2320 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour ocamlweb ...Gravatar letouzey2001-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2319 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli d'un quoteGravatar herbelin2001-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2318 85f007b7-540e-0410-9357-904b9bb8a0f7
* There remained traces of streams with the old syntax.Gravatar bertot2001-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrating the Ltac language and the Blast tool into the interfaceGravatar bertot2001-12-18
| | | | | | | | | | | | | capabilities: The Ltac language is the language that makes it possible to define new tactics without using the ocaml language (already present in coq for a few months). The Blast tool is a tool that checks whether the goals could be solve automatically and proposes the proof trace to the user. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2313 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo de parenthèsage + suppression de string (= str maintenant)Gravatar letouzey2001-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2311 85f007b7-540e-0410-9357-904b9bb8a0f7
* anti revolution culturelle: retour des arguments logiquesGravatar letouzey2001-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2310 85f007b7-540e-0410-9357-904b9bb8a0f7
* ote les redondances des entetesGravatar letouzey2001-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2309 85f007b7-540e-0410-9357-904b9bb8a0f7
* le save de Correctness faisant assert falseGravatar barras2001-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2300 85f007b7-540e-0410-9357-904b9bb8a0f7
* compat ocaml 3.03Gravatar filliatr2001-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction de bugs concernant la gestion des modules. debranchement du test ↵Gravatar letouzey2001-12-10
| | | | | | d'extraction sur les Reals en attendant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2282 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
* remise au gout du jour du repertoire theories/Sorting de la V6.3Gravatar letouzey2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2231 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make sure that NatRing won't loop forever.Gravatar bertot2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2226 85f007b7-540e-0410-9357-904b9bb8a0f7
* hack temporaire concernant les remarks/modulesGravatar letouzey2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2217 85f007b7-540e-0410-9357-904b9bb8a0f7
* iota généraliséGravatar letouzey2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2216 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'une méthode directe pour indiquer le type des déclarations ↵Gravatar herbelin2001-11-19
| | | | | | à toplevel plutôt que de passer par mkCast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage qualid_of_global en shortest_qualid_of_globalGravatar herbelin2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2201 85f007b7-540e-0410-9357-904b9bb8a0f7
* oubli: changement de nil en nilTGravatar mayero2001-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2192 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de list en listT, cons en consT et app en appTGravatar mayero2001-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2191 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revolution culturelle: suppression des arguments propGravatar letouzey2001-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2189 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moins de fichiers avec des axiomsGravatar letouzey2001-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des stamps et donc des *_constraintsGravatar clrenard2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite du petit oupsGravatar letouzey2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2185 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit oupsGravatar letouzey2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2184 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite refonte extraction.mlGravatar letouzey2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2182 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)Gravatar letouzey2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2181 85f007b7-540e-0410-9357-904b9bb8a0f7
* typoGravatar letouzey2001-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2175 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de l'optim singleton depuis extraction vers mlutil. Autres ↵Gravatar letouzey2001-11-08
| | | | | | modifs mineures git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2174 85f007b7-540e-0410-9357-904b9bb8a0f7
* epsilonGravatar letouzey2001-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refonte du fichier mlutil.ml. Correction d'un bug d'optim caseGravatar letouzey2001-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2167 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite des testsGravatar letouzey2001-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
* refonte du testGravatar letouzey2001-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2162 85f007b7-540e-0410-9357-904b9bb8a0f7
* optimisation consistant a parfois permuter case et funGravatar letouzey2001-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2161 85f007b7-540e-0410-9357-904b9bb8a0f7
* optim: Idset au lieu de listGravatar letouzey2001-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2160 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-11-05
| | | | | | | | | | - reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
* message non barbare si extraction dans une sectionGravatar letouzey2001-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2157 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement epsilonesqueGravatar letouzey2001-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2155 85f007b7-540e-0410-9357-904b9bb8a0f7
* retablissement de l'optim case constantGravatar letouzey2001-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2154 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout du script qualify2open qui met des open Truc en debut de fichierGravatar letouzey2001-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2153 85f007b7-540e-0410-9357-904b9bb8a0f7
* Creation de Recursive Extarction ModuleGravatar letouzey2001-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2152 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 10:57:52 +0000