Skip to content

Commit 550258d

Browse files
proux01proux01
committed
1 parent 07749eb commit 550258d

File tree

16 files changed

+45
-45
lines changed

16 files changed

+45
-45
lines changed

‎src/ADTNotation/BuildADT.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -340,8 +340,8 @@ Definition getMethDef
340340
methBody (ith methDefs idx).
341341

342342
(* Always simplify method lookup when the index is specified. *)
343-
Arguments getConsDef [_] {n} [_] _ idx%string / .
344-
Arguments getMethDef [_] {n} [_] _ idx%string / _ .
343+
Arguments getConsDef [_] {n} [_] _ idx%_string / .
344+
Arguments getMethDef [_] {n} [_] _ idx%_string / _ .
345345

346346
(* [BuildADT] constructs an ADT from a single constructor
347347
definition and a list of method signatures,

‎src/ADTNotation/BuildADTReplaceMethods.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -49,8 +49,8 @@ End ReplaceMethods.
4949
(* Always simplify method replacement when the index and new
5050
body are specified. *)
5151

52-
Arguments replaceConsDef [_ _ _] _ idx%string newDef%consDef / .
53-
Arguments ADTReplaceConsDef [_ _ _ _ _] _ _ idx%string newDef%consDef / .
52+
Arguments replaceConsDef [_ _ _] _ idx%_string newDef%_consDef / .
53+
Arguments ADTReplaceConsDef [_ _ _ _ _] _ _ idx%_string newDef%_consDef / .
5454

55-
Arguments replaceMethDef [_ _ _] _ idx%string newDef%methDef / .
56-
Arguments ADTReplaceMethDef [_ _ _ _ _] _ _ idx%string newDef%methDef / .
55+
Arguments replaceMethDef [_ _ _] _ idx%_string newDef%_methDef / .
56+
Arguments ADTReplaceMethDef [_ _ _ _ _] _ _ idx%_string newDef%_methDef / .

‎src/ADTNotation/BuildADTSig.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ Record consSig :=
77
{ consID : string;
88
consDom : list Type }.
99

10-
Arguments Build_consSig consID%string consDom%type_scope.
10+
Arguments Build_consSig consID%_string consDom%_type_scope.
1111
Bind Scope consSig_scope with consSig.
1212
Delimit Scope consSig_scope with consSig.
1313

@@ -17,7 +17,7 @@ Record methSig :=
1717
methCod : option Type
1818
}.
1919

20-
Arguments Build_methSig methID%string methDom%type_scope methCod%type_scope.
20+
Arguments Build_methSig methID%_string methDom%_type_scope methCod%_type_scope.
2121
Bind Scope methSig_scope with methSig.
2222
Delimit Scope methSig_scope with methSig.
2323

‎src/ADTNotation/BuildComputationalADT.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -303,8 +303,8 @@ Definition getcMethDef
303303
cMethBody (ith methDefs idx).
304304

305305
(* Always simplify method lookup when the index is specified. *)
306-
Arguments getcConsDef [_] {n} [_] _ idx%string / .
307-
Arguments getcMethDef [_] {n} [_] _ idx%string / _ .
306+
Arguments getcConsDef [_] {n} [_] _ idx%_string / .
307+
Arguments getcMethDef [_] {n} [_] _ idx%_string / _ .
308308

309309
(* [BuildcADT] constructs an computational ADT from a single constructor
310310
definition and a list of method signatures,

‎src/Common/BoundedLookup.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ Section BoundedIndex.
4848

4949
Global Arguments indexb {n Bound} b.
5050
Global Arguments bindex {n Bound} b.
51-
Global Arguments BoundedIndex {n} Bound%vector_scope.
51+
Global Arguments BoundedIndex {n} Bound%_vector_scope.
5252

5353
Lemma indexb_ibound_eq :
5454
forall n Bound (bidx bidx' : BoundedIndex (n := n) Bound),
@@ -346,7 +346,7 @@ Notation "x ++ y" := (Vector.append x y) : vector_scope.
346346
Notation "`` A" :=
347347
({| bindex := A%string |}) (at level 0, format "`` A").
348348

349-
Arguments BoundedString {n} _%vector_scope.
349+
Arguments BoundedString {n} _%_vector_scope.
350350

351351

352352

‎src/Common/EnumType.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,4 +26,4 @@ Coercion EnumType_inj_BoundedIndex : EnumType >-> BoundedIndex.
2626

2727
Notation "``` idx" := (BoundedIndex_inj_EnumType ``idx) (at level 0).
2828

29-
Global Arguments EnumType {len} {A} ta%vector_scope.
29+
Global Arguments EnumType {len} {A} ta%_vector_scope.

‎src/Common/PointedProp.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,14 +54,14 @@ Definition not_option_pointed_Prop (x : option pointed_Prop) : option pointed_Pr
5454
| None => Some trivial
5555
| Some (inject p) => Some (inject (~p))
5656
end.
57-
Arguments not_option_pointed_Prop _%option_pointed_prop.
57+
Arguments not_option_pointed_Prop _%_option_pointed_prop.
5858

5959
Definition and_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop
6060
:= match x, y with
6161
| Some x, Some y => Some (and_pointed_Prop x y)
6262
| _, _ => None
6363
end.
64-
Arguments and_option_pointed_Prop (_ _)%option_pointed_prop.
64+
Arguments and_option_pointed_Prop (_ _)%_option_pointed_prop.
6565

6666
Definition or_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop
6767
:= match x, y with
@@ -70,15 +70,15 @@ Definition or_option_pointed_Prop (x y : option pointed_Prop) : option pointed_P
7070
| None, Some y => Some y
7171
| None, None => None
7272
end.
73-
Arguments or_option_pointed_Prop (_ _)%option_pointed_prop.
73+
Arguments or_option_pointed_Prop (_ _)%_option_pointed_prop.
7474

7575
Definition impl_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop
7676
:= match x, y with
7777
| None, _ => Some trivial
7878
| Some x, Some y => Some (impl_pointed_Prop x y)
7979
| Some p, None => not_option_pointed_Prop p
8080
end.
81-
Arguments impl_option_pointed_Prop (_ _)%option_pointed_prop.
81+
Arguments impl_option_pointed_Prop (_ _)%_option_pointed_prop.
8282

8383
Infix "/\" := and_pointed_Prop : pointed_prop_scope.
8484
Infix "\/" := or_pointed_Prop : pointed_prop_scope.

‎src/Common/Wf1.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -368,8 +368,8 @@ for fixn in range(1, 11):
368368
Definition Fix%(fixn)d_Proper_eq_with_assumption : Fix%(fixn)d_Proper_eq_with_assumption'T := Fix%(fixn)d_Proper_eq_with_assumption'.
369369
End Fix%(fixn)d.
370370
371-
Arguments Fix%(fixn)d_Proper_eq {%(letters)s R Rwf P} %(fix_underscores)s.
372-
Arguments Fix%(fixn)d_Proper_eq_with_assumption {%(letters)s R Rwf P} _ _ %(fix_underscores)s.
371+
Arguments Fix%_(fixn)d_Proper_eq {%_(letters)s R Rwf P} %_(fix_underscores)s.
372+
Arguments Fix%_(fixn)d_Proper_eq_with_assumption {%_(letters)s R Rwf P} _ _ %_(fix_underscores)s.
373373
Global Existing Instance Fix%(fixn)d_Proper_eq.
374374
Global Existing Instance Fix%(fixn)d_Proper_eq_with_assumption.
375375
""" % locals())

‎src/Common/Wf2.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -570,8 +570,8 @@ for fixn in range(1, 11):
570570
Definition Fix%(fixn)d_2_%(fixn)d_eq : Fix%(fixn)d_2_%(fixn)d_eq'T := Fix%(fixn)d_2_%(fixn)d_eq'.
571571
End Fix2_%(fixn)d.
572572
573-
Arguments Fix2_%(fixn)d_Proper_eq {A A' %(letters)s R Rwf P} %(fix_underscores)s.
574-
Arguments Fix2_%(fixn)d_Proper_eq_with_assumption {A A' %(letters)s R Rwf P} _ _ %(fix_underscores)s.
573+
Arguments Fix2_%_(fixn)d_Proper_eq {A A' %_(letters)s R Rwf P} %_(fix_underscores)s.
574+
Arguments Fix2_%_(fixn)d_Proper_eq_with_assumption {A A' %_(letters)s R Rwf P} _ _ %_(fix_underscores)s.
575575
Global Existing Instance Fix2_%(fixn)d_Proper_eq.
576576
Global Existing Instance Fix2_%(fixn)d_Proper_eq_with_assumption.
577577
""" % locals())

‎src/Computation/Core.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,8 @@ Definition Bind2 (A B C: Type)
2626

2727

2828
Bind Scope comp_scope with Comp.
29-
Arguments Bind [A%type B%type] ca%comp k%comp _.
30-
Arguments Bind2 [A%type B%type C%type] c%comp k%comp _.
29+
Arguments Bind [A%_type B%_type] ca%_comp k%_comp _.
30+
Arguments Bind2 [A%_type B%_type C%_type] c%_comp k%_comp _.
3131
Arguments Return [_] _ _.
3232
Arguments Pick [_] _ _.
3333

0 commit comments

Comments
 (0)