From 3b640b68c89f1e9fcbb0f98c8865819189409382 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 27 Sep 2017 16:37:03 +0200
Subject: Code factorization Vernacentries.interp on VernacProof.

---
 vernac/vernacentries.ml | 25 +++++++------------------
 1 file changed, 7 insertions(+), 18 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4af4b642ca..66427b7093 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 *)
-- 
cgit v1.2.3