aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)Author
2002-10-07Lazy manuelles dans le codecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07Make sure that bin/parser exists when checking that it worksbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3094 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-05Lazy experimentale temporaire...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-02*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3068 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Adding the congruence closure tactics (CC and CCsolve).corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3033 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3016 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-19Pretty-printing preliminaire des modules, commandescoq
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
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2947 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2944 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-29*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2931 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-18*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2896 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-17ajout de make otags utilisant otags plutot que etagsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2892 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-17modification de make tags pourletouzey
1) eviter de parser les fichiers de contrib/extraction/test et de depasser les capacitees de etags 2) supprimer les tags ne venant pas des regexps fournis (--language=none) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2891 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Makefile pour Realsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2881 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15code retour de make checkcourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2872 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2859 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2840 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2817 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2816 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-25*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2804 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-20*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2800 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-19deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwffilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2795 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-17*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2788 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-11*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2775 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07extraction vers schemeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07Adding file theories/ZArith/Zsqrt.v that contains a square root function.bertot
actually three functions are provided, one working on positive numbers (it is structurally recursive), one with a strong specification (Zsqrt), and one with a weak specification (Zsqrt_plain). For the function with a weak specification an extra theorem is also provided. The decision functions in ZArith_dec have been made transparent so that computation with the square root function also becomes possible with Lazy Beta Iota Delta Zeta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2770 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; ↵herbelin
rparation de la protection contre les clauses indiscernables de TACTIC EXTEND et VERNAC COMMAND EXTEND; rparation des grammaires de Extraction, EAuto, TextMode, KillProof et Derive Dependent Inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2753 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-04*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2752 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-04'make check' echoue si au moins un test echoue.courant
Les distributions binaires ne peuvent etre faites que si 'make check' reussit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2751 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
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
2002-05-29Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2712 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-15integration de coq-inferior par Marco Maggesifilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2645 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-05nouveau module Zdivfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2614 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-04resolution du pb d'efficacite du a Sign.add_named_declbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-27*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2569 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-22An intuitionistic first-order theorem prover -- JProver.huang
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
2002-03-13cleanconfig efface ocamldebug-v7filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2529 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-12*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2525 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-05ajout d'une entree 'binaries' pour recompiler coq mais pas les theoriesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2515 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Big commit extraction:letouzey
- 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
2002-02-20Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parceddr
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
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de ↵letouzey
contrib/omega vers theories/ZArith git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2406 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-10MAJ ocaml 3.04 sur Windowsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2387 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19suppression de commentaires obsoletesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2346 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19contrib/interface/dad.ml4 had no real need of streams, it should have beenbertot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 21:24:37 +0000