diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 6 | ||||
| -rw-r--r-- | tools/coqdep.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 8 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 4 |
4 files changed, 12 insertions, 8 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 5231899c6e..fb064c495f 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -184,7 +184,7 @@ CMOFILES = \ $(MLPACKFILES:.mlpack=.cmo) CMXFILES = $(CMOFILES:.cmo=.cmx) OFILES = $(CMXFILES:.cmx=.o) -CMAFILES = $(MLLIBFILES:.mllib=.cma) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) CMXAFILES = $(CMAFILES:.cma=.cmxa) CMIFILES = \ $(CMOFILES:.cmo=.cmi) \ @@ -474,6 +474,10 @@ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx $(SHOW)'CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 930b092d3b..044399544a 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -495,7 +495,7 @@ let coqdep () = add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); let coqlib = Envars.coqlib () in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 4e4b33c322..9723905790 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -40,7 +40,7 @@ let is_keyword = "Hypothesis"; "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite"; "Implicit"; "Import"; "Inductive"; - "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; + "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Locate"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes"; @@ -62,9 +62,9 @@ let is_keyword = (*i (* coq terms *) *) "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; - "fix"; "cofix"; + "fix"; "cofix"; "is"; (* Ltac *) - "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; + "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; "type"; "of"; "rec"; (* Notations *) "level"; "associativity"; "no" ] @@ -74,7 +74,7 @@ let is_tactic = [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; - "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; + "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; "quote"; "eexact"; "autorewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 288e7e1e51..cd04665cc1 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -230,7 +230,7 @@ let declare_loading_string () = \n Mltop.set_top\ \n {Mltop.load_obj=\ \n (fun f -> if not (Topdirs.load_file ppf f)\ -\n then CErrors.error (\"Could not load plugin \"^f));\ +\n then CErrors.user_err Pp.(str (\"Could not load plugin \"^f)));\ \n Mltop.use_file=Topdirs.dir_use ppf;\ \n Mltop.add_dir=Topdirs.dir_directory;\ \n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ @@ -260,7 +260,7 @@ let create_tmp_main_file modules = let main () = let (options, userfiles) = parse_args () in (* Directories: *) - let () = Envars.set_coqlib ~fail:CErrors.error in + let () = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)) in let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in (* Which ocaml compiler to invoke *) let prog = if !opt then "opt" else "ocamlc" in |