diff options
| -rw-r--r-- | Makefile.extr | 6 | ||||
| -rw-r--r-- | backend/Regalloc.ml | 4 | ||||
| -rw-r--r-- | cparser/pre_parser.mly | 2 | ||||
| -rw-r--r-- | cparser/validator/Alphabet.v | 4 |
4 files changed, 10 insertions, 6 deletions
diff --git a/Makefile.extr b/Makefile.extr index 503c6a6a..fbc119de 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -38,9 +38,13 @@ INCLUDES=$(patsubst %,-I %, $(DIRS)) # warning 3 = deprecated feature. Turned off for OCaml 4.02 (bytes vs strings) # warning 20 = unused function argument. There are some in extracted code -WARNINGS=-w +a-4-9-27-29 -strict-sequence -safe-string -warn-error +a +WARNINGS=-w +a-3-4-9-27-29 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03 extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45 +cparser/pre_parser.cmx: WARNINGS += -w -41 +cparser/pre_parser.cmo: WARNINGS += -w -41 +backend/CMparser.cmx: WARNINGS += -w -41 +backend/CMparser.cmo: WARNINGS += -w -41 COMPFLAGS+=-g $(INCLUDES) $(MENHIR_INCLUDES) $(WARNINGS) diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index e531a34a..3432b79d 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -1123,7 +1123,7 @@ and success f alloc = end; f' -open Errors +open !Errors let regalloc f = init_trace(); @@ -1131,7 +1131,7 @@ let regalloc f = let f1 = Splitting.rename_function f in match RTLtyping.type_function f1 with | Error msg -> - Error(MSG (coqstring_of_camlstring "RTL code after splitting is ill-typed:") :: msg) + Errors.Error(MSG (coqstring_of_camlstring "RTL code after splitting is ill-typed:") :: msg) | OK tyenv -> let f2 = function_of_RTL_function f1 tyenv in let liveness = liveness_analysis f2 in diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly index 21008f1c..27502a3b 100644 --- a/cparser/pre_parser.mly +++ b/cparser/pre_parser.mly @@ -23,7 +23,7 @@ *) %{ - open Pre_parser_aux + open !Pre_parser_aux let set_id_type (_,r,_) t = r := t diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v index 13718cd5..db850860 100644 --- a/cparser/validator/Alphabet.v +++ b/cparser/validator/Alphabet.v @@ -199,8 +199,8 @@ Next Obligation. apply Zcompare_antisym. Qed. Next Obligation. destruct c. unfold compare31 in *. rewrite Z.compare_eq_iff in *. congruence. -eapply Zcompare_Lt_trans; eauto. -eapply Zcompare_Gt_trans; eauto. +eapply Zcompare_Lt_trans. apply H. apply H0. +eapply Zcompare_Gt_trans. apply H. apply H0. Qed. Next Obligation. intros x y H. unfold compare, compare31 in H. |