diff options
| author | Kathy Gray | 2014-02-27 14:01:59 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-02-27 14:01:59 +0000 |
| commit | bfe28e3e443fd28e7182cfeff1cf8b5fa5bc4e5a (patch) | |
| tree | 715adfee820c1b59b0db2fd93f2614b07a69c8c9 /language/Makefile | |
| parent | 88a18f8abc20fc1b421d22ed06a75a51bb293414 (diff) | |
| parent | 7582bed6349cd05d7237168a39d5dad99ede7e38 (diff) | |
Merge branch 'interp_typed'
Conflicts:
src/lem_interp/interp.lem
src/lem_interp/run_interp.ml
Diffstat (limited to 'language/Makefile')
| -rw-r--r-- | language/Makefile | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/language/Makefile b/language/Makefile index d650f957..2076069c 100644 --- a/language/Makefile +++ b/language/Makefile @@ -9,7 +9,7 @@ all: l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem %Theory.uo: %Script.sml Holmake --qof -I $(OTTLIB) $@ -l2.tex: l2.ott l2_rules.ott +l2.tex: l2.ott l2_typ.ott l2_rules.ott ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ %.tex: %.ott @@ -21,12 +21,8 @@ l2.tex: l2.ott l2_rules.ott %Script.sml: %.ott ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ -%.lem: %.ott - # work around what is probably a bug in -generate_aux_rules true: when we try to generate Lem code with - # that turned on, we get some surprising-looking parse failures in a - # few rules. Likely we're not doing the proper transform for rules - # generated from inductive relation syntax. - ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ +l2.lem: l2.ott l2_typ.ott + ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ clean: rm -rf *~ |