aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Collapse)Author
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
2001-12-19reparation du make depend et du .dependletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Add a new file in the files needed for the "coq-interface" binary: the filebertot
contrib/interface/blast.cmo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2315 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-10- condition de garde (suite)barras
- commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2274 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2271 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2260 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2259 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2258 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2256 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2245 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Possibilité d'appeler check avec l'option -byteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2235 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 00:25:08 +0000