summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml26
-rw-r--r--tools/coqdoc/cpretty.mll20
-rw-r--r--tools/coqdoc/index.ml6
-rw-r--r--tools/coqdoc/output.ml8
-rw-r--r--tools/win32hack.mllib1
-rw-r--r--tools/win32hack_filename.ml4
6 files changed, 40 insertions, 25 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index a685d6ea..20117ca6 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -315,10 +315,10 @@ in
print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "%.g: %.v\n\t$(GALLINA) $<\n\n";
- print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n";
- print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n";
- print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n";
- print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n";
+ print "%.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
+ print "%.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
+ print "%.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n";
+ print "%.g.html: %.v %.glob\n\t$(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@\n\n";
print "%.v.d: %.v\n";
print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
print "%.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n"
@@ -349,11 +349,13 @@ let variables is_install opt (args,defs) =
print "\n";
end;
(* Coq executables and relative variables *)
+ if !some_vfile || !some_mlpackfile || !some_mllibfile then
+ print "COQDEP?=$(COQBIN)coqdep -c\n";
if !some_vfile then begin
print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
print "COQCHKFLAGS?=-silent -o\n";
+ print "COQDOCFLAGS?=-interpolate -utf8\n";
print "COQC?=$(COQBIN)coqc\n";
- print "COQDEP?=$(COQBIN)coqdep -c\n";
print "GALLINA?=$(COQBIN)gallina\n";
print "COQDOC?=$(COQBIN)coqdoc\n";
print "COQCHK?=$(COQBIN)coqchk\n\n";
@@ -374,7 +376,7 @@ let variables is_install opt (args,defs) =
print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n";
print "GRAMMARS?=grammar.cma\n";
print "CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
- print "CAMLP4OPTIONS?=\n";
+ print "CAMLP4OPTIONS?=-loc loc\n";
print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n\n";
end;
match is_install with
@@ -564,18 +566,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
print "gallina: $(GFILES)\n\n";
print "html: $(GLOBFILES) $(VFILES)\n";
print "\t- mkdir -p html\n";
- print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
print "\t- mkdir -p html\n";
- print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
print "all.ps: $(VFILES)\n";
- print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "all-gal.ps: $(VFILES)\n";
- print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "all.pdf: $(VFILES)\n";
- print "\t$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "all-gal.pdf: $(VFILES)\n";
- print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "validate: $(VOFILES)\n";
print "\t$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))\n\n";
print "beautify: $(VFILES:=.beautified)\n";
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 89047e83..925f5258 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -306,7 +306,12 @@ let thm_token =
let prf_token =
"Next" space+ "Obligation"
- | "Proof" (space* "." | space+ "with")
+ | "Proof" (space* "." | space+ "with" | space+ "using")
+
+let immediate_prf_token =
+ (* Approximation of a proof term, if not in the prf_token case *)
+ (* To be checked after prf_token *)
+ "Proof" space* [^ '.' 'w' 'u']
let def_token =
"Definition"
@@ -382,7 +387,8 @@ let commands =
| ("Hypothesis" | "Hypotheses")
| "End"
-let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+let end_kw =
+ immediate_prf_token | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
let extraction =
"Extraction"
@@ -504,7 +510,7 @@ rule coq_bol = parse
output_indented_keyword s lexbuf;
let eol= body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | space* notation_kw space*
+ | space* notation_kw
{ let s = lexeme lexbuf in
output_indented_keyword s lexbuf;
let eol= start_notation_string lexbuf in
@@ -605,7 +611,7 @@ and coq = parse
| prf_token
{ let eol =
if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
+ begin backtrack lexbuf; body lexbuf end
else
let s = lexeme lexbuf in
let eol =
@@ -631,7 +637,7 @@ and coq = parse
Output.ident s (lexeme_start lexbuf);
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | notation_kw space*
+ | notation_kw
{ let s = lexeme lexbuf in
Output.ident s (lexeme_start lexbuf);
let eol= start_notation_string lexbuf in
@@ -1096,7 +1102,7 @@ and body = parse
if eol
then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
else body lexbuf }
- | "where" space*
+ | "where"
{ Tokens.flush_sublexer();
Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
start_notation_string lexbuf }
@@ -1120,6 +1126,8 @@ and body = parse
body lexbuf }
and start_notation_string = parse
+ | space { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
+ start_notation_string lexbuf }
| '"' (* a true notation *)
{ Output.sublexer '"' (lexeme_start lexbuf);
notation_string lexbuf;
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index c8e7770a..f19433e9 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -62,7 +62,7 @@ let add_def loc1 loc2 ty sp id =
for loc = loc1 to loc2 do
Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty))
done;
- Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
+ Hashtbl.add deftable id (Def (full_ident sp id, ty))
let add_ref m loc m' sp id ty =
if Hashtbl.mem reftable (m, loc) then ()
@@ -289,11 +289,11 @@ let all_entries () =
let l = try Hashtbl.find bt t with Not_found -> [] in
Hashtbl.replace bt t ((s,m) :: l)
in
- let classify (m,_) e = match e with
+ let classify m e = match e with
| Def (s,t) -> add_g s m t; add_bt t s m
| Ref _ | Mod _ -> ()
in
- Hashtbl.iter classify reftable;
+ Hashtbl.iter classify deftable;
Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
{ idx_name = "global";
idx_entries = sort_entries !gl;
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index e3d5741a..3aed28b4 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -29,14 +29,14 @@ let build_table l =
let is_keyword =
build_table
- [ "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+ [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
"CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
- "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
+ "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar"; "Goal"; "Hint";
"Hypothesis"; "Hypotheses";
"Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
"Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
"Module"; "Module Type"; "Declare Module"; "Include";
- "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
+ "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "Proof"; "Proof with"; "Qed";
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
"Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
"Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
@@ -44,7 +44,7 @@ let is_keyword =
"Delimit"; "Bind"; "Open"; "Scope"; "Inline";
"Implicit Arguments"; "Add"; "Strict";
"Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
- "subgoal";
+ "subgoal"; "vm_compute";
"Opaque"; "Transparent";
(* Program *)
"Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
diff --git a/tools/win32hack.mllib b/tools/win32hack.mllib
new file mode 100644
index 00000000..42395f65
--- /dev/null
+++ b/tools/win32hack.mllib
@@ -0,0 +1 @@
+Win32hack_filename \ No newline at end of file
diff --git a/tools/win32hack_filename.ml b/tools/win32hack_filename.ml
new file mode 100644
index 00000000..74f70686
--- /dev/null
+++ b/tools/win32hack_filename.ml
@@ -0,0 +1,4 @@
+(* The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/".
+ Let's tweak that... *)
+
+let _ = Filename.dir_sep.[0] <- '\\'
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-07 07:51:49 +0000