[doc] attribute #[using]

5 files changed, 12 insertions, 7 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index c55a7928d9..efba6d332a 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -229,6 +229,6 @@ let uses_parser : string key_parser = fun orig args ->
   assert_once ~name:"using" orig;
   match args with
   | VernacFlagLeaf str -> str
-  |  _ -> CErrors.user_err (Pp.str "Ill formed uses attribute")
+  |  _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute")
 
 let using = attribute_of_list ["using",uses_parser]
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index aa71e58cf6..3fc74cba5b 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -121,7 +121,8 @@ let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ct
   let using = using |> Option.map (fun expr ->
     let terms = body :: match types with Some x -> [x] | None -> [] in
     let l = Proof_using.process_expr (Global.env()) evd expr terms in
-    Names.Id.Set.(List.fold_right add l empty)) in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let kind = Decls.IsDefinition kind in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
   let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
@@ -140,7 +141,8 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red
   let using = using |> Option.map (fun expr ->
     let terms = body :: match types with Some x -> [x] | None -> [] in
     let l = Proof_using.process_expr (Global.env()) evd expr terms in
-    Names.Id.Set.(List.fold_right add l empty)) in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
     let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index bd11fa2b47..29bf5fbcc2 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -263,7 +263,8 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps =
           let env = Global.env() in
           let sigma = Evd.from_env env in
           let l = Proof_using.process_expr env sigma expr terms in
-          Names.Id.Set.(List.fold_right add l empty)) in
+          Names.Id.Set.(List.fold_right add l empty))
+        in
         let args = List.map Context.Rel.Declaration.get_name ctx in
         Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
       ) fixnames fixtypes fiximps
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index c2e07c4fd5..9623317ddf 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -262,7 +262,8 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notat
   let using = using |> Option.map (fun expr ->
     let terms = List.map EConstr.of_constr [evars_def; evars_typ] in
     let l = Proof_using.process_expr env sigma expr terms in
-    Names.Id.Set.(List.fold_right add l empty)) in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let uctx = Evd.evar_universe_context sigma in
   let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
   let info = Declare.Info.make ~udecl ~poly ~hook () in
@@ -294,7 +295,8 @@ let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
     let using = using |> Option.map (fun expr ->
       let terms = [def; typ] in
       let l = Proof_using.process_expr env evd expr terms in
-      Names.Id.Set.(List.fold_right add l empty)) in
+      Names.Id.Set.(List.fold_right add l empty))
+    in
     let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b6e7d22732..bc03994ca6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -501,7 +501,7 @@ let program_inference_hook env sigma ev =
 let vernac_set_used_variables ~pstate e : Declare.Proof.t =
   let env = Global.env () in
   let sigma, _ = Declare.Proof.get_current_context pstate in
-  let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
+  let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
   let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
   let l = Proof_using.process_expr env sigma e tys in
   let vars = Environ.named_context env in