diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 6 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 8 |
2 files changed, 9 insertions, 5 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/coqdoc/output.ml b/tools/coqdoc/output.ml index 82d3d62b59..e06ef9d765 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -36,7 +36,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"; @@ -58,9 +58,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" ] @@ -70,7 +70,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"; |