diff options
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index fa9ba1d..db5b7bc 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -494,18 +494,6 @@ Definition binary_constructor_correct eval_expr ge e le m b vb -> eval_expr ge e le m c v. -(* -Definition binary_constructor_correct' - (make: expr -> type -> expr -> type -> res expr) - (sem: val -> val -> option val): Prop := - forall a tya b tyb c va vb v e le m, - sem va vb = Some v -> - make a tya b tyb = OK c -> - eval_expr ge e le m a va -> - eval_expr ge e le m b vb -> - eval_expr ge e le m c v. -*) - Lemma make_add_correct: binary_constructor_correct make_add sem_add. Proof. red; intros until m. intro SEM. unfold make_add. |