diff options
| -rw-r--r-- | vernac/vernacentries.ml | 25 |
1 files changed, 7 insertions, 18 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4af4b642c..66427b709 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2060,24 +2060,13 @@ let interp ?proof ?loc locality poly c = | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, using) -> - begin match Option.append using (Proof_using.get_default_proof_using ()) with - | None -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:no" - | Some l -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:yes"; - vernac_set_used_variables l - end - | VernacProof (Some tac, using) -> - begin match Option.append using (Proof_using.get_default_proof_using ()) with - | None -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:no"; - vernac_set_end_tac tac - | Some l -> - Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes"; - vernac_set_end_tac tac; - vernac_set_used_variables l - end + | VernacProof (tac, using) -> + let using = Option.append using (Proof_using.get_default_proof_using ()) in + let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in + let usings = if Option.is_empty using then "using:no" else "using:yes" in + Aux_file.record_in_aux_at ?loc "VernacProof" (tacs^" "^usings); + Option.iter vernac_set_end_tac tac; + Option.iter vernac_set_used_variables using | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] (* Extensions *) |