diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-27 16:37:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-10 23:50:25 +0200 |
| commit | 3b640b68c89f1e9fcbb0f98c8865819189409382 (patch) | |
| tree | 9bedcfcf03302c54dc66248e2839f19b8575d1e0 /vernac | |
| parent | 7f1635816588ae200c8eed381d726bd29f57d899 (diff) | |
Code factorization Vernacentries.interp on VernacProof.
Diffstat (limited to 'vernac')
| -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 *) |