diff options
Diffstat (limited to 'vernac/proof_using.ml')
| -rw-r--r-- | vernac/proof_using.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 094e2c1184..cfb3248c7b 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -130,7 +130,7 @@ let suggest_common env ppid used ids_typ skip = str "should start with one of the following commands:"++spc()++ v 0 ( prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs)); - if !Flags.record_aux_file + if Aux_file.recording () then let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) in record_proof_using s |