Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit ef1146ce authored by David Monniaux's avatar David Monniaux
Browse files

Compatibilité Coq 8.13

parent 71d69df1
......@@ -27,8 +27,6 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL Linking.
Declare Scope option_monad_scope.
Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
(at level 200, X ident, A at level 100, B at level 200)
: option_monad_scope.
......@@ -105,13 +105,12 @@ with hsmem_proj hm :=
| HSstore hm chk addr hl hv _ => Sstore (hsmem_proj hm) chk addr (hsval_list_proj hl) (hsval_proj hv)
Declare Scope hse.
Local Open Scope hse.
(** We use a Notation instead a Definition, in order to get more automation "for free" *)
Notation "'seval_hsval' ge sp hsv" := (seval_sval ge sp (hsval_proj hsv))
(only parsing, at level 0, ge at next level, sp at next level, hsv at next level): hse.
Local Open Scope hse.
Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_list_proj lhv))
(only parsing, at level 0, ge at next level, sp at next level, lhv at next level): hse.
Notation "'seval_hsmem' ge sp hsm" := (seval_smem ge sp (hsmem_proj hsm))
......@@ -273,8 +273,6 @@ 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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment