diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:59:44 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:59:44 +0200 |
| commit | 4c379d48b35e7c8156f3953fede31d5e47faf8ca (patch) | |
| tree | fa19eb30178fcf74b0768d9f5df4017ab6afc770 /backend/SplitLongproof.v | |
| parent | 3b79923a6c9fa8c76916df1eecfdecd7ae2124a5 (diff) | |
| download | compcert-kvx-4c379d48b35e7c8156f3953fede31d5e47faf8ca.tar.gz compcert-kvx-4c379d48b35e7c8156f3953fede31d5e47faf8ca.zip | |
helpers broke compilation
Diffstat (limited to 'backend/SplitLongproof.v')
| -rw-r--r-- | backend/SplitLongproof.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index df77b322..b13bd1f7 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -23,8 +23,6 @@ Require Import SelectOp SelectOpproof SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. -<<<<<<< HEAD -======= (** * Properties of the helper functions *) Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := @@ -47,7 +45,6 @@ Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l. ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. @@ -60,10 +57,7 @@ Variable sp: val. Variable e: env. Variable m: mem. -<<<<<<< HEAD Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto. -======= ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: |