make sanity_check pass (Deducteam#1072)

fblanqui · Mar 29, 2024 · 9eab1da · 9eab1da
1 parent e30b979
commit 9eab1da
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 10 deletions.
diff --git a/src/export/coq.ml b/src/export/coq.ml
@@ -97,7 +97,8 @@ let set_erasing : string -> unit = fun f ->
         let id = snd lp_qid.elt in
         if Logger.log_enabled() then log "erase %s" id;
         erase := StrSet.add id !erase;
-        map_erased_qid_coq := QidMap.add lp_qid.elt coq_id !map_erased_qid_coq;
+        map_erased_qid_coq :=
+          QidMap.add lp_qid.elt coq_id !map_erased_qid_coq;
         if fst lp_qid.elt = [] && id <> coq_id then
           rmap := StrMap.add id coq_id !rmap
     | {pos;_} -> fatal pos "Invalid command."

diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml
@@ -137,7 +137,8 @@ let rec remove_wraps ({elt;_} as t) =
 let rule : p_rule pp =
   let varset ppf set = List.pp string ", " ppf (StrSet.elements set) in
   fun ppf {elt=(l,r);_} ->
-  out ppf "[%a] %a --> %a.@." varset (pvars_lhs l) term (remove_wraps l) term r
+  out ppf "[%a] %a --> %a.@."
+    varset (pvars_lhs l) term (remove_wraps l) term r
 
 let partition_modifiers ms =
   let ms = List.map (fun {elt;_} -> elt) ms in

diff --git a/src/handle/command.ml b/src/handle/command.ml
@@ -515,8 +515,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
             wrn pe.pos "Proof admitted.";
             (* Keep the definition only if the symbol is not opaque. *)
             let d =
-              if opaq then None
-              else Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term
+              if opaq then None else
+                Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term
             in
             (* Add the symbol in the signature. *)
             fst (Sig_state.add_symbol
@@ -527,8 +527,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
               fatal pe.pos "The proof is not finished:@.%a" goals ps;
             (* Keep the definition only if the symbol is not opaque. *)
             let d =
-              if opaq then None
-              else Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term
+              if opaq then None else
+                Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term
             in
             (* Add the symbol in the signature. *)
             Console.out 2 (Color.red "symbol %a : %a") uid id term a;

diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml
@@ -383,9 +383,9 @@ let rec handle :
        | Typ gt::_ ->
          Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt
        | _ -> assert false)
-  | P_tac_try tactic -> 
-    try handle ss sym_pos prv ps tactic 
-    with Fatal(_, _s) -> ps 
+  | P_tac_try tactic ->
+    try handle ss sym_pos prv ps tactic
+    with Fatal(_, _s) -> ps
 
 (** Representation of a tactic output. *)
 type tac_output = proof_state * Query.result

diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml
@@ -280,7 +280,7 @@ let rec tactic : p_tactic pp = fun ppf { elt;  _ } ->
   | P_tac_simpl (Some qid) -> out ppf "simplify %a" qident qid
   | P_tac_solve -> out ppf "solve"
   | P_tac_sym -> out ppf "symmetry"
-  | P_tac_try t -> out ppf "try %a" tactic t 
+  | P_tac_try t -> out ppf "try %a" tactic t
   | P_tac_why3 p ->
       let prover ppf s = out ppf " \"%s\"" s in
       out ppf "why3%a" (Option.pp prover) p