diff --git a/theories/proto/proto_def.v b/theories/proto/proto_def.v
index 72af0d64b78d946d7dac492a153758593e780fab..17a5e6ff350ba41fef0e6445c179119bd0d269d0 100644
--- a/theories/proto/proto_def.v
+++ b/theories/proto/proto_def.v
@@ -21,7 +21,7 @@ Arguments TEnd {_ _}.
 Arguments TSR {_ _} _ _ _.
 Instance: Params (@TSR) 3.
 
-Instance stype_inhabited V A : Inhabited (proto V A) := populate TEnd.
+Instance proto_inhabited V A : Inhabited (proto V A) := populate TEnd.
 
 CoFixpoint dual_proto {V A} (prot : proto V A) : proto V A :=
   match prot with