mit-pdos · tchajed · Sep 6, 2024 · Sep 6, 2024
diff --git a/_CoqProject b/_CoqProject
@@ -2,6 +2,8 @@
 -arg -w -arg -ssr-search-moved
 -arg -w -arg +deprecated-instance-without-locality
 -arg -w -arg -future-coercion-class-field
+# don't allow ambiguous coercions
+-arg -w -arg +ambiguous-paths
 -arg -w -arg +deprecated-hint-rewrite-without-locality
 -arg -w -arg -deprecated-field-instance-without-locality
 -arg -w -arg +deprecated-tactic-notation

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/comments.v b/external/Goose/github_com/goose_lang/goose/internal/examples/comments.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* 0consts.go *)
 

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/rfc1813.v b/external/Goose/github_com/goose_lang/goose/internal/examples/rfc1813.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition PROGRAM : expr := #(U32 100003).
 

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/simpledb.v b/external/Goose/github_com/goose_lang/goose/internal/examples/simpledb.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* Package simpledb implements a one-table version of LevelDB
 

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import.v b/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import.v
@@ -4,7 +4,6 @@ From Perennial.goose_lang.trusted Require Import github_com.goose_lang.goose.int
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Bar: val :=
   rec: "Bar" <> :=

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v b/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Foo: val :=
   rec: "Foo" <> :=

diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/unittest/generic.v b/external/Goose/github_com/goose_lang/goose/internal/examples/unittest/generic.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition SliceMap (T:ty) (U:ty): val :=
   rec: "SliceMap" "f" "s" :=

diff --git a/external/Goose/github_com/goose_lang/std.v b/external/Goose/github_com/goose_lang/std.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* BytesEqual returns if the two byte slices are equal. *)
 Definition BytesEqual: val :=

diff --git a/external/Goose/github_com/mit_pdos/go_journal/alloc.v b/external/Goose/github_com/mit_pdos/go_journal/alloc.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* Allocator uses a bit map to allocate and free numbers. Bit 0
    corresponds to number 0, bit 1 to 1, and so on. *)

diff --git a/external/Goose/github_com/mit_pdos/go_journal/lockmap.v b/external/Goose/github_com/mit_pdos/go_journal/lockmap.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* lockmap is a sharded lock map.
 

diff --git a/external/Goose/github_com/mit_pdos/go_journal/util.v b/external/Goose/github_com/mit_pdos/go_journal/util.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Debug : expr := #0.
 

diff --git a/external/Goose/github_com/mit_pdos/go_nfsd/nfstypes.v b/external/Goose/github_com/mit_pdos/go_nfsd/nfstypes.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition PROGRAM : expr := #(U32 100003).
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/bank.v b/external/Goose/github_com/mit_pdos/gokv/bank.v
@@ -6,7 +6,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition BAL_TOTAL : expr := #1000.
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/example.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/example.v
@@ -7,7 +7,6 @@ From Goose Require github_com.mit_pdos.gokv.dmvcc.txnmgr.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition main: val :=
   rec: "main" <> :=

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/index.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/index.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.vmvcc.index.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* 0_server.go *)
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/prophname.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/prophname.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Get: val :=
   rec: "Get" <> :=

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txn.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txn.v
@@ -8,7 +8,6 @@ From Perennial.goose_lang.trusted Require Import github_com.mit_pdos.vmvcc.trust
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Clerk := struct.decl [
   "p" :: ProphIdT;

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txncoordinator.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txncoordinator.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.gokv.dmvcc.index.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* 0_server.go *)
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txnmgr.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txnmgr.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* clerk.go *)
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/erpc.v b/external/Goose/github_com/mit_pdos/gokv/erpc.v
@@ -5,7 +5,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* Implements "exactly-once RPCs" with a reply table. *)
 

diff --git a/external/Goose/github_com/mit_pdos/gokv/kv.v b/external/Goose/github_com/mit_pdos/gokv/kv.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Kv := struct.decl [
   "Put" :: (stringT -> stringT -> unitT)%ht;

diff --git a/external/Goose/github_com/mit_pdos/gokv/lockservice.v b/external/Goose/github_com/mit_pdos/gokv/lockservice.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.gokv.kv.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition LockClerk := struct.decl [
   "kv" :: ptrT

diff --git a/external/Goose/github_com/mit_pdos/gokv/map_marshal.v b/external/Goose/github_com/mit_pdos/gokv/map_marshal.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition EncodeMapU64ToU64: val :=
   rec: "EncodeMapU64ToU64" "kvs" :=

diff --git a/external/Goose/github_com/mit_pdos/gokv/map_string_marshal.v b/external/Goose/github_com/mit_pdos/gokv/map_string_marshal.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition EncodeStringMap: val :=
   rec: "EncodeStringMap" "kvs" :=

diff --git a/external/Goose/github_com/mit_pdos/gokv/tutorial/basics.v b/external/Goose/github_com/mit_pdos/gokv/tutorial/basics.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Tracker := struct.decl [
   "mu" :: ptrT;

diff --git a/external/Goose/github_com/mit_pdos/gokv/tutorial/queue.v b/external/Goose/github_com/mit_pdos/gokv/tutorial/queue.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Queue := struct.decl [
   "queue" :: slice.T uint64T;

diff --git a/external/Goose/github_com/mit_pdos/gokv/vrsm/e.v b/external/Goose/github_com/mit_pdos/gokv/vrsm/e.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation Error := uint64T (only parsing).
 

diff --git a/external/Goose/github_com/mit_pdos/pav/cryptoffi.v b/external/Goose/github_com/mit_pdos/pav/cryptoffi.v
@@ -2,7 +2,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition HashLen : expr := #32.
 

diff --git a/external/Goose/github_com/mit_pdos/pav/cryptoutil.v b/external/Goose/github_com/mit_pdos/pav/cryptoutil.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.pav.cryptoffi.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation Hasher := (slice.T byteT) (only parsing).
 

diff --git a/external/Goose/github_com/mit_pdos/pav/marshalutil.v b/external/Goose/github_com/mit_pdos/pav/marshalutil.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation errorTy := boolT (only parsing).
 

diff --git a/external/Goose/github_com/mit_pdos/pav/merkle.v b/external/Goose/github_com/mit_pdos/pav/merkle.v
@@ -6,7 +6,6 @@ From Goose Require github_com.mit_pdos.pav.cryptoutil.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation errorTy := boolT (only parsing).
 

diff --git a/external/Goose/github_com/mit_pdos/perennial_examples/alloc.v b/external/Goose/github_com/mit_pdos/perennial_examples/alloc.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition unit := struct.decl [
 ].

diff --git a/external/Goose/github_com/mit_pdos/rsm/distx.v b/external/Goose/github_com/mit_pdos/rsm/distx.v
@@ -4,7 +4,6 @@ From Goose Require github_com.goose_lang.std.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Value := struct.decl [
   "b" :: boolT;

diff --git a/external/Goose/github_com/mit_pdos/rsm/mpaxos.v b/external/Goose/github_com/mit_pdos/rsm/mpaxos.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Paxos := struct.decl [
 ].