diff options
Diffstat (limited to 'scheduling/AbstractBasicBlocksDef.v')
| -rw-r--r-- | scheduling/AbstractBasicBlocksDef.v | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/scheduling/AbstractBasicBlocksDef.v b/scheduling/AbstractBasicBlocksDef.v index 6960f363..34d72de1 100644 --- a/scheduling/AbstractBasicBlocksDef.v +++ b/scheduling/AbstractBasicBlocksDef.v @@ -273,23 +273,26 @@ with list_term := Scheme term_mut := Induction for term Sort Prop with list_term_mut := Induction for list_term Sort Prop. +Declare Scope pattern_scope. +Declare Scope term_scope. Bind Scope pattern_scope with term. Delimit Scope term_scope with term. Delimit Scope pattern_scope with pattern. +Local Open Scope pattern_scope. + Notation "[ ]" := (LTnil _) (format "[ ]"): pattern_scope. -Notation "[ x ]" := (LTcons x [] _): pattern_scope. +Notation "[ x ]" := (LTcons x [ ] _): pattern_scope. Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil _) _) .. _) _): pattern_scope. Notation "o @ l" := (App o l _) (at level 50, no associativity): pattern_scope. Import HConsingDefs. Notation "[ ]" := (LTnil unknown_hid) (format "[ ]"): term_scope. -Notation "[ x ]" := (LTcons x [] unknown_hid): term_scope. +Notation "[ x ]" := (LTcons x []%term unknown_hid): term_scope. Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil unknown_hid) unknown_hid) .. unknown_hid) unknown_hid): term_scope. Notation "o @ l" := (App o l unknown_hid) (at level 50, no associativity): term_scope. -Local Open Scope pattern_scope. Fixpoint term_eval (ge: genv) (t: term) (m: mem): option value := match t with @@ -370,7 +373,7 @@ Qed. Hint Resolve intro_fail_correct: wlp. (** The default reduction of a term to a pseudo-term *) -Definition identity_fail (t: term):= intro_fail [t] t. +Definition identity_fail (t: term):= intro_fail (t::nil) t. Lemma identity_fail_correct (t: term): match_pt t (identity_fail t). Proof. @@ -382,8 +385,8 @@ Hint Resolve identity_fail_correct: wlp. (** The reduction for constant term *) Definition nofail (is_constant: op -> bool) (t: term):= match t with - | Input x _ => intro_fail ([])%list t - | o @ [] => if is_constant o then (intro_fail ([])%list t) else (identity_fail t) + | Input x _ => intro_fail nil t + | o @ [] => if is_constant o then (intro_fail nil t) else (identity_fail t) | _ => identity_fail t end. |