Merge remote-tracking branch 'dk/master' into db

editors/emacs/lambdapi-mode.el

@@ -194,9 +194,6 @@
    '(lambdapi-mode . ("lambdapi" "lsp" "--standard-lsp")))
   (eglot-ensure)
 
-  ;; set column offsets for lambdapi's LSP server
-  (setq-local eglot-move-to-column-function #'eglot-move-to-column)
-
   ;; Hooks for goals
   (add-hook 'post-command-hook #'lambdapi-update-line-number nil :local)
   ;; Hook binding line change to re-execution of proof/goals

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."

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

src/handle/command.ml

@@ -499,8 +499,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
@@ -511,8 +511,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;

src/handle/tactic.ml

@@ -393,9 +393,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

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