diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-04 22:21:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-04 22:21:28 +0000 |
| commit | c20bdd9c7b3d0823f1c2fb3bbb56fa12d3ca88dd (patch) | |
| tree | 04c61223c47da7ba6c50a47ce0cf02074f4d150a | |
| parent | 50a4cdd38f3c80306b1f200c699dd6504d2b410a (diff) | |
Added installation of .cmi files in "make install" target of coq_makefile.
Updated CHANGES.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11747 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | tools/coq_makefile.ml4 | 15 |
2 files changed, 11 insertions, 6 deletions
@@ -336,6 +336,8 @@ Tactics occurrences of a term. - Tactic "pose proof" supports name overwriting in case of specialization of an hypothesis. +- Semi-decision tactic "jp" for first-order intuitionistic logic moved to user + contributions (subsumed by "firstorder"). Program diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index dcb220ea2..4135a370e 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -185,6 +185,7 @@ let install (vfiles,mlfiles,_,sds) inc = print "\tmkdir -p $(COQLIB)/user-contrib\n"; if !some_vfile then install_include_by_root "VOFILES" vfiles inc; if !some_mlfile then install_include_by_root "CMOFILES" mlfiles inc; + if !some_mlfile then install_include_by_root "CMIFILES" mlfiles inc; if Coq_config.has_natdynlink && !some_mlfile then install_include_by_root "CMXSFILES" mlfiles inc; List.iter @@ -389,6 +390,7 @@ let main_targets vfiles mlfiles other_targets inc = print "CMOFILES:=$(MLFILES:.ml=.cmo)\n"; classify_files_by_root "CMOFILES" mlfiles inc; print "CMIFILES:=$(MLFILES:.ml=.cmi)\n"; + classify_files_by_root "CMIFILES" mlfiles inc; print "CMXFILES:=$(MLFILES:.ml=.cmx)\n"; print "CMXSFILES:=$(MLFILES:.ml=.cmxs)\n"; classify_files_by_root "CMXSFILES" mlfiles inc; @@ -471,8 +473,6 @@ let rec process_cmd_line = function some_vfile := true else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then some_mlfile := true - else - () in List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies); Special (file,dependencies,com) :: (process_cmd_line r) @@ -498,10 +498,13 @@ let rec process_cmd_line = function some_vfile := true; V f :: (process_cmd_line r) end else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then begin - some_mlfile := true; - ML f :: (process_cmd_line r) - end else - Subdir f :: (process_cmd_line r) + some_mlfile := true; + ML f :: (process_cmd_line r) + end else if (Filename.check_suffix f ".mli") then begin + Printf.eprintf "Warning: no need for .mli files, skipped %s\n" f; + process_cmd_line r + end else + Subdir f :: (process_cmd_line r) let banner () = print (Printf.sprintf |