aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
Commit message (Collapse)AuthorAge
* Remove useless MonoList.vGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12339 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Tentatively made order-dependency wrt .vo files a full dependencyGravatar herbelin2009-09-15
| | | | | | | | | | | of the doc (use "make QUICK=1" to shortcut it) otherwise, the compilation of the doc is re-checked only when the doc files are removed. - Fixed a typo in coqdoc.sty and a redundancy in Makefile.common . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12334 85f007b7-540e-0410-9357-904b9bb8a0f7
* Addendum to revision 12323; update Makefile.common after removal ofGravatar herbelin2009-09-11
| | | | | | | | ExternalProvers.tex in revision 12320. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12324 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 ↵Gravatar fbesson2009-08-25
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delegate _all_ doc targets to stage2Gravatar lmamane2009-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12293 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parsing files for numerals (+ ascii/string) moved into pluginsGravatar letouzey2009-03-27
| | | | | | | | | | | | | | Idea: make coqtop more independant of the standard library. In the future, we can imagine loading the syntax for numerals right after their definition. For the moment, it is easier to stay lazy and load the syntax plugins slightly before the definitions. After this commit, the main (sole ?) references to theories/ from the core ml files are in Coqlib (but many parts of coqlib are only used by plugins), and it mainly concerns Init (+ Logic/JMeq and maybe a few others). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
* make coqdep_boot in stage1, not stage2Gravatar lmamane2009-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12014 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild improvements + minor makefile fixGravatar letouzey2009-03-24
| | | | | | | | | | | * a small shell script ./build to drive ocamlbuild * rules for all the binaries (apart from coqide and coqchk) * use of ocamlbuild's Echo instead of using shell + sed + awk for generated files * Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the list of things to "clean" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
* pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file)Gravatar letouzey2009-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
| | | | | | | | | | | | | | | | | | | | | | | | * generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵Gravatar letouzey2009-03-20
| | | | | | user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
* missing -c option of ocamlc in coq_makefile; coqdep_boot main loop was ↵Gravatar barras2009-03-16
| | | | | | included in coqdep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11985 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdep_boot: a specialized and dependency-free coqdep for killing one of the ↵Gravatar letouzey2009-03-16
| | | | | | build stages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: fix ignored errors, several attempts to clarify thingsGravatar letouzey2009-03-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | * I encountered error messages during compilation, for instance ocamlopt complaining about non-existing coq_config.cmi when compiling coq_config.ml. Moreover, make was _not_ stopping at these errors (WTF?!). After some debug, it turned out to be (indirectly) my fault: I placed earlier the inclusion of the new .mllib.d in Makefile.stage1, but this is too early, coqdep, which is used to compute these files, isn't built yet. Due to the semantics of "-include", make tries to build it, fails with the above error, and goes on happily. Arrgh. After moving the inclusion of these .mllib.d to Makefile.stage2, everything seems to work ok now. * Since we're using such "nice" non-trivial features of make, I've started a small FAQ section about them at the beginning of Makefile * Recursive calls to make are now done with two options: --no-builtin-rules : let's avoid builtin rules like "%:%.o" ... --warn-undefined-variable : using a non-defined variable isn't necessarily bad, but I found a few bugs with this option, and I suggest we keep it. * Clarified the rules about stage* in Makefile and their STAGE*_TARGETS variables in Makefile.common. Now a newcomer _might_ have a chance to grasp in less than a day what's going on ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: minor improvementsGravatar letouzey2009-03-16
| | | | | | | | * no need anymore for special rules for -rectypes: we use it everywhere * $(REVISIONCMO) is obsolete * avoid triple references to almost all files of kernel/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better mechanism for loading initial pluginsGravatar letouzey2009-03-14
| | | | | | | | | | | | | | | | Instead of dirty hacks in toplevel/coqtop.ml, we simply add some Declare ML Module in Prelude.v. Gain: now that coqdep is clever enough, dependencies are automatic, and we can simplify the Makefile quite a lot: no more references to INITPLUGINSBEST and the like. Besides, mltop.ml4 can also be simplified a lot: by giving $(CONTRIBSTATIC) to coqmktop instead of contrib.cma, now coqtop is aware that it already contain the static plugins (or not), and subsequent ML Module are ignored correctly without us having to do anything :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11979 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: ml dependencies of contribs are moved to .mllib filesGravatar letouzey2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
* - per session coq command stackGravatar vgross2009-03-07
| | | | | | | | | | | - removed circular dependency between record and class used to keep track of sessions => no need for mutable option in record. - more 'a option ref pruning - more code splitting - more alpha-rewriting git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11968 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de la tactique groebner de Loic PottierGravatar barras2009-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11964 85f007b7-540e-0410-9357-904b9bb8a0f7
* porting r11900 11905 and 11953 to trunkGravatar barras2009-03-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11954 85f007b7-540e-0410-9357-904b9bb8a0f7
* Heavy modifications on the widget and edition tab creation mechanism.Gravatar vgross2009-03-02
| | | | | | | | Overloading of GPack.notebook => Vector no longer needed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: avoid building an empty contrib.cmxaGravatar letouzey2009-02-27
| | | | | | | | Patch suggested by Yves. Now that the list of contrib to link statically in coqtop can be empty, we should avoid trying to build an empty contrib.cmxa, since this fails at least on MacOS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11947 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqInterface.vo in CONTRIBVO (should fix a dependency issue)Gravatar letouzey2009-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11943 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq-interface and coq-parser can be calls to coqtop with adequate code dynlinkGravatar letouzey2009-02-20
| | | | | | | | | | | | | | | | From files in contrib/interface, we create (if natdynlink is available) two plugins named coqinterface_plugin.{cma,cmxs} and coqparser_plugin.{cma,cmxs}. These plugins are loaded respectively by CoqInterface.v and CoqParser.v. So coq-interface can be "coqtop -require CoqInterface", and coq-parser can be "coqtop -batch -l CoqParser" (this one cannot be compiled into a .vo, otherwise a customized toplevel is launched during the compilation). Turing coq-interface and coq-parser and their .opt versions into shell scripts allow to spare around 40 Mb of disk space... Nota: at dynlink, parse.ml was conflicting with the module Parse of the ocaml runtime, so I renamed it into coqparser.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backport of 11890 from branch v8.2 (compile tools with the bestGravatar herbelin2009-02-11
| | | | | | | available compiler) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11922 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix de divers petits problèmes d'installationGravatar notin2009-02-11
| | | | | | (cherry picked from commit 998a9a62874ba6cf26bdfe28f3ef0c72deaf0c25) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification du style du manuel de référenceGravatar notin2009-02-11
| | | | | | (cherry picked from commit b44a87556b68c08b7cd2fcbdaf2b4067b8a77427) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report des revisions #11826, #11828 et #11829 de v8.2 vers trunkGravatar notin2009-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow to turn contrib/subtac into a (nat)dynlink'able pluginGravatar letouzey2009-02-03
| | | | | | | | | | | | | | | | | | | Main issue was declare_summary being triggered too late in subtac_obligations, hence the associated init_function was _not_ being done by Lib.init(). Fixed for the moment by an ad-hoc launch of this init_function in subtac_obligations. In other plugins, this issue doesn't appear, since init_function is mostly putting back some empty set into a reference that was initially empty. No need to really run init_function in this case. For future plugins, we will nonetheless have to be careful about that. Of course, the (ref Obj.magic) was not exactly helpful in debugging this matter, see http://caml.inria.fr/mantis/view.php?id=4707 As said by Xavier, naughty naughty boys... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the installation of plugins (both initial and late ones)Gravatar letouzey2009-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de cp --parents par un script shGravatar notin2009-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11833 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
| | | | | | | unplugged a long time ago. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11798 85f007b7-540e-0410-9357-904b9bb8a0f7
* DISCLAIMERGravatar puech2009-01-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ========== This big patch is commited here with a HUGE experimental tag on it. It is probably not a finished job. The aim of committing it now, as agreed with Hugo, is to get some feedback from potential users to identify more clearly the directions the implementation could take. So please feel free to mail me any remarks, bug reports or advices at <puech@cs.unibo.it>. Here are the changes induced by it : For the user ============ * Search tools have been reimplemented to be faster and more general. Affected are [SearchPattern], [SearchRewrite] and [Search] (not [SearchAbout] yet). Changes are: - All of them accept general constructions, and previous syntactical limitations are abolished. In particular, one can for example [SearchPattern (nat -> Prop)], which will find [isSucc], but also [le], [gt] etc. - Patterns are typed. This means that you cannot search mistyped expressions anymore. I'm not sure if it's a good or a bad thing though (especially regarding coercions)... * New tool to automatically infer (some) Record/Typeclasses instances. Usage : [Record/Class *Infer* X := ...] flags a record/class as subject to instance search. There is also an option to activate/deactivate the search [Set/Unset Autoinstance]. It works by finding combinations of definitions (actually all kinds of objects) which forms a record instance, possibly parameterized. It is activated at two moments: - A complete search is done when defining a new record, to find all possible instances that could have been formed with past definitions. Example: Require Import List. Record Infer Monoid A (op:A->A->A) e := { assoc : forall x y z, op x (op y z) = op (op x y) z; idl : forall x, x = op x e ; idr : forall x, x = op e x }. new instance Monoid_autoinstance_1 : (Monoid nat plus 0) [...] - At each new declaration (Definition, Axiom, Inductive), a search is made to find instances involving the new object. Example: Parameter app_nil_beg : forall A (l:list A), l = nil ++ l. new instance Build_Monoid_autoinstance_12 : (forall H : Type, Monoid (list H) app nil) := (fun H : Type => Build_Monoid (list H) app nil ass_app (app_nil_beg H) (app_nil_end H)) For the developper ================== * New yet-to-be-named datastructure in [lib/dnet.ml]. Should do efficient one-to-many or many-to-one non-linear first-order filtering, faster than traditional methods like discrimination nets (so yes, the name of the file should probably be changed). * Comes with its application to Coq's terms [pretyping/term_dnet.ml]. Terms are represented so that you can search for patterns under products as fast as you would do not under products, and facilities are provided to express other kind of searches (head of application, under equality, whatever you need that can be expressed as a pattern) * A global repository of all objects defined and imported is maintained [toplevel/libtypes.ml], with all search facilities described before. * A certain kind of proof search in [toplevel/autoinstance.ml]. For the moment it is specialized on finding instances, but it should be generalizable and reusable (more on this in a few months :-). The bad news ============ * Compile time should increase by 0 to 15% (depending on the size of the Requires done). This could be optimized greatly by not performing substitutions on modules which are not functors I think. There may also be some inefficiency sources left in my code though... * Vo's also gain a little bit of weight (20%). That's inevitable if I wanted to store the big datastructure of objects, but could also be optimized some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Workaround to compile the coq archive with dynamic loading on Mac OS 10.5Gravatar herbelin2009-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11777 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed the recompilation of config/revision.ml once every two conmpilations.Gravatar herbelin2009-01-10
| | | | | | | | - Fixed an error message in configure - Support for filenames with spaces in coqmktop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11772 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor doc fixes:Gravatar msozeau2009-01-08
| | | | | | | | | | | - Set BIBINPUTS variable correctly so that we do not use any random biblio.bib file. - Update setoid_rewrite doc to new typeclasses syntax and fix verb -> texttt - Stop using less than 100% line heights in coqdoc.css git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite de la révision #11756Gravatar notin2009-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11757 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conversion du fichier 'revision' en un fichier .ml + correction d'un bug ↵Gravatar notin2009-01-06
| | | | | | dans le configure introduit par les révisions 11754 et 11755 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision 11754 (compilation sous windows)Gravatar notin2009-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11755 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved JProver to a user contribution (as was decided a long time ago)Gravatar herbelin2009-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11746 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
| | | | | | | | | | | | | of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take advantage of natdynlink when available: almost all contribs become ↵Gravatar letouzey2008-12-16
| | | | | | | | | | | | | | | | | | | | | | | | loadable plugins - Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode). - Features that were available without any Require are now loaded systematically when launching coqtop (see Coqtop.load_initial_plugins): extraction, jprover, cc, ground, dp, recdef, xml - The other plugins are loaded when a corresponding Require is done: quote, ring, field, setoid_ring, omega, romega, micromega, fourier - I experienced a crash (segfault) while turning subtac into a plugin, so this one stays statically linked into coqtop for now - When the ocaml version doesn't support natdynlink, or if "-natdynlink no" is explicitely given to configure, coqtop is statically linked with all of the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear. - How should coqdep handle a "Declare ML Module "foo"" if foo is an archive and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the same location as the .v during the build, but can be moved later in any place of the ml loadpath. This is clearly an experimentation. Feedback most welcome... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move FunctionalExtensionality to Logic/ (someone please check that theGravatar msozeau2008-12-16
| | | | | | | | | | doc is ok). Rework the .v files in Program accordingly, adding some documentation and proper headers. Integrate the development of an elimination principle for measured functions in Program/Wf by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1995Gravatar notin2008-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Native "Declare ML Module" when possibleGravatar glondu2008-10-28
| | | | | | | | | Dynlink.add_{interfaces,available_units} are deprecated and not implemented natively. Currently, native "Declare ML Module" doesn't work because of this. Dynlink-related should be switched to the API introduced in OCaml 3.07. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11518 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)Gravatar herbelin2008-10-18
| | | | | | | | | - Makefile: typo apparente avec .ml4.preprocessed - test-suite: ajout d'un test sur eta qui trainait dans le coin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11465 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not install csdpcert in $(BINDIR)Gravatar glondu2008-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11388 85f007b7-540e-0410-9357-904b9bb8a0f7
* Install coqide manpageGravatar glondu2008-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11372 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-31 17:17:27 +0000