diff --git a/CHANGES.md b/CHANGES.md
index c6cd899f4339ccd0057869f639bef3bf4d5364ce..4bd8c218965f5d854c6e13d9b897a1155a250c3d 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -8,6 +8,12 @@ Standard library
       - in `set.SetApp` and `set.SetImp`, type `t` becomes `set`;
         field `contents` becomes `to_fset`; call to `empty` becomes `empty ()`
 
+Language
+  * It is now possible to give a name to requires and assertions.
+    `requires Hyp { a = 3 }` tries to give the name `Hyp` to the corresponding
+    hypothesis after introduction. This uses the attribute [@hyp_name:] which is
+    now reserved.
+
 Tools
   * counterexamples given by `why3prove` are no longer printed using JSON
     by default; pass option `--json` to restore the previous behavior
diff --git a/src/core/ident.ml b/src/core/ident.ml
index bb69d4d801ef91aa34e38be23ff53d031aa9d6e8..4b46cb57201951e68707a8f3ed0a6e1bd539c1b0 100644
--- a/src/core/ident.ml
+++ b/src/core/ident.ml
@@ -450,6 +450,15 @@ let extract_field attr =
   with
   | _ -> None
 
+(* Attributes used to name hypothesis *)
+let is_hyp_name_attr a =
+  Strings.has_prefix "hyp_name:" a.attr_string
+
+let get_hyp_name ~attrs =
+  try Some (Strings.remove_prefix "hyp_name:"
+              (Sattr.choose (Sattr.filter is_hyp_name_attr attrs)).attr_string)
+  with Not_found -> None
+
 (* Functions for working with ITP attributes *)
 
 let is_name_attr a =
diff --git a/src/core/ident.mli b/src/core/ident.mli
index 6133c9436165524282e722677ce260a890cb4060..1fe837d08a92fa2ace9bb54cb1ad9af75a577151 100644
--- a/src/core/ident.mli
+++ b/src/core/ident.mli
@@ -232,3 +232,7 @@ val extract_field: attribute -> (int * string) option
 val get_model_trace_attr : attrs:Sattr.t -> attribute
 (** Return an attribute of the form ["model_trace:*"].
     Raises [Not_found] if there is no such attribute. *)
+
+val get_hyp_name: attrs:Sattr.t -> string option
+(** If attrs contains an attribute of the form ["hyp_name:<s>"] returns
+    [Some <s>] or [None] if no attribute have this form *)
diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index ec263030febdbd3f0332507634342a55f814fae9..1f3e4714341ffee612e3a6440594440dd7ee738c 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -1082,8 +1082,13 @@ single_expr_:
     { Ematch ($2, [], $4) }
 | GHOST single_expr
     { Eghost $2 }
-| assertion_kind LEFTBRC term RIGHTBRC
-    { Eassert ($1, $3) }
+| assertion_kind option(name) LEFTBRC term RIGHTBRC
+    { match $2 with
+      | None -> Eassert ($1, $4)
+      | Some name ->
+         let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ name)) in
+         let t = { $4 with term_desc = Tattr (attr, $4) } in
+         Eassert ($1, t) }
 | attr single_expr %prec prec_attr
     { Eattr ($1, $2) }
 | single_expr cast
@@ -1182,9 +1187,18 @@ spec:
 | (* epsilon *) %prec prec_no_spec  { empty_spec }
 | single_spec spec                  { spec_union $1 $2 }
 
+name:
+| LIDENT { $1 }
+| UIDENT { $1 }
+
 single_spec:
-| REQUIRES LEFTBRC term RIGHTBRC
-    { { empty_spec with sp_pre = [$3] } }
+| REQUIRES option(name) LEFTBRC term RIGHTBRC
+    { match $2 with
+      | None -> { empty_spec with sp_pre = [$4] }
+      | Some name ->
+         let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ name)) in
+         let t = { $4 with term_desc = Tattr (attr, $4) } in
+         { empty_spec with sp_pre = [t] } }
 | ENSURES LEFTBRC ensures RIGHTBRC
     { { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
 | RETURNS LEFTBRC match_cases(term) RIGHTBRC
diff --git a/src/transform/introduction.ml b/src/transform/introduction.ml
index 6f45df60330abfbe3cb9033560dd00fdb556905a..a1d31dad7416114db20977a48d7b803706301021 100644
--- a/src/transform/introduction.ml
+++ b/src/transform/introduction.ml
@@ -120,7 +120,9 @@ let rec intros kn pr mal expl f =
       (* f is going to be removed, preserve its attributes and location in f2 *)
       let f2 = t_attr_copy f f2 in
       let fl = Split_goal.split_intro_right ?known_map:kn (dequant false f1) in
-      let idx = id_fresh "H" ~attrs:intro_attrs in
+      let idx =
+        let name = Ident.get_hyp_name ~attrs:f1.t_attrs in
+        id_fresh (Opt.get_def "H" name) ~attrs:intro_attrs in
       let add (subst,dl) f =
         let svs = Mvs.set_diff (t_freevars Mvs.empty f) subst in
         let subst, dl = Mvs.fold (fun vs _ (subst,dl) ->