aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/C2C.ml18
-rw-r--r--cfrontend/Cexec.v12
-rw-r--r--cfrontend/Cminorgenproof.v2
-rw-r--r--cfrontend/Cshmgen.v4
-rw-r--r--cfrontend/Ctypes.v4
-rw-r--r--cfrontend/SimplExpr.v4
6 files changed, 24 insertions, 20 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index f2fbf255..6a33c48d 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -16,6 +16,8 @@
open C
open Camlcoq
+open Floats
+open Values
open Ctypes
open Csyntax
@@ -366,8 +368,8 @@ let globals_for_strings globs =
let constant_size_t a =
match Initializers.constval_cast !comp_env a Ctyping.size_t with
- | Errors.OK(Values.Vint n) -> Some(Integers.Int.unsigned n)
- | Errors.OK(Values.Vlong n) -> Some(Integers.Int64.unsigned n)
+ | Errors.OK(Vint n) -> Some(Integers.Int.unsigned n)
+ | Errors.OK(Vlong n) -> Some(Integers.Int64.unsigned n)
| _ -> None
let make_builtin_memcpy args =
@@ -444,7 +446,7 @@ let make_builtin_va_arg env ty e =
"__compcert_va_composite" ty e
| _ ->
unsupported "va_arg at this type";
- Eval(Values.Vint(coqint_of_camlint 0l), type_int32s)
+ Eval(Vint(coqint_of_camlint 0l), type_int32s)
(** ** Translation functions *)
@@ -630,9 +632,9 @@ let convertFloat f kind =
| Z.Z0 ->
begin match kind with
| FFloat ->
- Ctyping.econst_single (Floats.Float.to_single Floats.Float.zero)
+ Ctyping.econst_single (Float.to_single Float.zero)
| FDouble | FLongDouble ->
- Ctyping.econst_float Floats.Float.zero
+ Ctyping.econst_float Float.zero
end
| Z.Zpos mant ->
@@ -647,11 +649,11 @@ let convertFloat f kind =
begin match kind with
| FFloat ->
- let f = Floats.Float32.from_parsed base mant exp in
+ let f = Float32.from_parsed base mant exp in
checkFloatOverflow f "float";
Ctyping.econst_single f
| FDouble | FLongDouble ->
- let f = Floats.Float.from_parsed base mant exp in
+ let f = Float.from_parsed base mant exp in
checkFloatOverflow f "double";
Ctyping.econst_float f
end
@@ -660,7 +662,7 @@ let convertFloat f kind =
(** Expressions *)
-let ezero = Eval(Values.Vint(coqint_of_camlint 0l), type_int32s)
+let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s)
let ewrap = function
| Errors.OK e -> e
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 4dcf2a47..a9ffcd3d 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -130,8 +130,8 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
Ltac mydestr :=
match goal with
- | [ |- None = Some _ -> _ ] => intro X; discriminate
- | [ |- Some _ = Some _ -> _ ] => intro X; inv X
+ | [ |- None = Some _ -> _ ] => let X := fresh "X" in intro X; discriminate
+ | [ |- Some _ = Some _ -> _ ] => let X := fresh "X" in intro X; inv X
| [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
| [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
| [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
@@ -2038,12 +2038,14 @@ Definition do_step (w: world) (s: state) : list transition :=
Ltac myinv :=
match goal with
- | [ |- In _ nil -> _ ] => intro X; elim X
+ | [ |- In _ nil -> _ ] => let X := fresh "X" in intro X; elim X
| [ |- In _ (ret _ _) -> _ ] =>
+ let X := fresh "X" in
intro X; elim X; clear X;
- [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
+ [let EQ := fresh "EQ" in intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
| [ |- In _ (_ :: nil) -> _ ] =>
- intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv]
+ let X := fresh "X" in
+ intro X; elim X; clear X; [let EQ := fresh "EQ" in intro EQ; inv EQ; myinv | myinv]
| [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv
| [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv
| [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index ea1bc89c..a6d58f17 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -20,7 +20,7 @@ Require Import AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Csharpminor Switch Cminor Cminorgen.
-Open Local Scope error_monad_scope.
+Local Open Scope error_monad_scope.
Definition match_prog (p: Csharpminor.program) (tp: Cminor.program) :=
match_program (fun cu f tf => transl_fundef f = OK tf) eq p tp.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index aeb31fe2..792a73f9 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -24,8 +24,8 @@ Require Import Coqlib Maps Errors Integers Floats.
Require Import AST Linking.
Require Import Ctypes Cop Clight Cminor Csharpminor.
-Open Local Scope string_scope.
-Open Local Scope error_monad_scope.
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
(** * Csharpminor constructors *)
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 0794743d..8d6cdb24 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -1064,7 +1064,7 @@ Proof.
destruct (complete_members env m) eqn:C; simplify_eq EQ. clear EQ; intros EQ.
rewrite PTree.gsspec. intros [A|A]; auto.
destruct (peq id id0); auto.
- inv A. rewrite <- H1; auto.
+ inv A. rewrite <- H0; auto.
}
intros. exploit REC; eauto. rewrite PTree.gempty. intuition congruence.
Qed.
@@ -1519,7 +1519,7 @@ Local Transparent Linker_program.
- intros. exploit link_match_fundef; eauto. intros (tf & A & B). exists tf; auto.
- intros.
Local Transparent Linker_types.
- simpl in *. destruct (type_eq v1 v2); inv H4. subst v tv2. exists tv1; rewrite dec_eq_true; auto.
+ simpl in *. destruct (type_eq v1 v2); inv H4. exists v; rewrite dec_eq_true; auto.
- eauto.
- eauto.
- eauto.
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 71b67f67..8725edd1 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -38,8 +38,8 @@ Inductive result (A: Type) (g: generator) : Type :=
| Err: Errors.errmsg -> result A g
| Res: A -> forall (g': generator), Ple (gen_next g) (gen_next g') -> result A g.
-Implicit Arguments Err [A g].
-Implicit Arguments Res [A g].
+Arguments Err [A g].
+Arguments Res [A g].
Definition mon (A: Type) := forall (g: generator), result A g.
generated by cgit (git 2.34.1) at 2024-07-08 06:07:28 +0000