Commit 5b3d90c3 authored by Francois Bobot's avatar Francois Bobot
Browse files

enable_coq_support = yes <=> include .depend.coq

parent 0ab81636
...@@ -371,8 +371,9 @@ src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4 ...@@ -371,8 +371,9 @@ src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4
$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@ $(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@
# depend and clean targets # depend and clean targets
ifeq (@enable_coq_support@,yes)
include .depend.coq include .depend.coq
endif
.depend.coq: $(COQGENERATED) .depend.coq: $(COQGENERATED)
$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@ $(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@
......
...@@ -11,7 +11,7 @@ unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown" ...@@ -11,7 +11,7 @@ unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
(* À discuter *) (* À discuter *)
transformation "simplify_recursive_definition" transformation "simplify_recursive_definition"
transformation "inline_trivial" (*transformation "inline_trivial"*)
transformation "eliminate_builtin" transformation "eliminate_builtin"
transformation "eliminate_definition" transformation "eliminate_definition"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment