aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Collapse)AuthorAge
* majGravatar filliatr2002-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3114 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3104 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the congruence closure tactics (CC and CCsolve).Gravatar corbinea2002-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3058 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3050 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3027 85f007b7-540e-0410-9357-904b9bb8a0f7
* La notation with dependante + affichage dependante de moduels corrigeGravatar coq2002-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3022 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3021 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3020 85f007b7-540e-0410-9357-904b9bb8a0f7
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ .dependGravatar coq2002-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2974 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pretty-printing preliminaire des modules, commandesGravatar coq2002-08-19
| | | | | | | | | | | | | Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bugs TautoGravatar courant2002-07-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2905 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug Tauto : la regle pour (A->B)->C echouait quand C etaitGravatar courant2002-07-15
| | | | | | | de la forme (E->F)->G. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2868 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2799 85f007b7-540e-0410-9357-904b9bb8a0f7
* extraction vers schemeGravatar letouzey2002-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
* affaiblissement hyp de Zmult_reg_leftGravatar filliatr2002-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
* jLogic disparaîtGravatar herbelin2002-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2660 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar courant2002-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2649 85f007b7-540e-0410-9357-904b9bb8a0f7
* backtrack dans l'algo d'unificationGravatar barras2002-04-10
| | | | | | | fichier usage incorrect (libdir et bindir ont disparu) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2629 85f007b7-540e-0410-9357-904b9bb8a0f7
* An intuitionistic first-order theorem prover -- JProver.Gravatar huang2002-03-22
| | | | | | | See the "README" file for more information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2563 85f007b7-540e-0410-9357-904b9bb8a0f7
* MakefileGravatar courant2002-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2523 85f007b7-540e-0410-9357-904b9bb8a0f7
* Big commit extraction:Gravatar letouzey2002-03-04
| | | | | | | | | | | - Changement de syntaxe (Extraction Language Toplevel/Ocaml/Haskell) - Retour des inductifs singletons et vides dans extraction.ml (extraction.ml -> actions sur le type, mlutil.ml -> conserve le type) - maintenant par defaut Recursive Extraction === Extraction "file" - kill_prop global est fait dans extraction.ml selon typage (a suivre...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2508 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parceGravatar ddr2002-02-20
| | | | | | | | qu'il entre en conflit avec le module Errors ajouté dans OCaml courant (future version OCaml 3.05). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2489 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
| | | | | | | - coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
* substitution et pattern modulo letGravatar barras2002-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement generation de schema d'elimination, False_rec est primitif, ↵Gravatar mohring2002-01-31
| | | | | | Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2404 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
* 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
* MAJGravatar herbelin2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2333 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation de make doc (ocamlweb & _)Gravatar letouzey2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add dependencies for two new files in contrib/interfaceGravatar bertot2001-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise a jour des dependancesGravatar clrenard2001-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2249 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2001-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2248 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@2245 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2001-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2244 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
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un fichier Max dans Arith, et enrichissement du Min.Gravatar letouzey2001-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2195 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
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 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
* Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ↵Gravatar letouzey2001-10-26
| | | | | | ETC etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2141 85f007b7-540e-0410-9357-904b9bb8a0f7
* chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les ↵Gravatar letouzey2001-10-22
| | | | | | options git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2133 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 04:23:15 +0000