update ciclib+format

src/ciclib/const.mli

@@ -1,6 +1,6 @@
 (** Constants.
 
-  Constants are logical symbols, defined by the user thanks to an open type *)
+    Constants are logical symbols, defined by the user thanks to an open type *)
 
 open Types_
 

src/ciclib/level.mli

@@ -39,16 +39,15 @@ val subst : subst -> t -> t
 
 (** {2 Judgements}
 
-    These are little proofs of some symbolic properties of levels, even
-    those which contain variables. *)
+    These are little proofs of some symbolic properties of levels, even those
+    which contain variables. *)
 
 val judge_leq : t -> t -> bool
-(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower
-    or equal to [l2] *)
+(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower or equal to
+    [l2] *)
 
 val judge_eq : t -> t -> bool
-(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2]
-    and [judge_leq l2 l1] *)
+(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2] and [judge_leq l2 l1] *)
 
 val judge_is_zero : t -> bool
 (** [judge_is_zero st l] is [true] iff [l <= 0] holds *)

src/ciclib/term.ml

@@ -190,9 +190,9 @@ let db_shift_ (e : term) (n : int) =
         map_shallow e ~f:(fun inbind u ->
             loop u
               (if inbind then
-                k + 1
-              else
-                k))
+                 k + 1
+               else
+                 k))
     )
   in
   assert (n >= 0);
@@ -225,9 +225,9 @@ let db_replace_ e (env : t list) : term =
         map_shallow e ~f:(fun inb u ->
             aux u
               (if inb then
-                k + 1
-              else
-                k))
+                 k + 1
+               else
+                 k))
     )
   in
   if is_closed e then

src/ciclib/term.mli

@@ -1,11 +1,11 @@
 (** Core logic terms.
 
-  The core terms are expressions in the calculus of constructions,
-  with no universe polymorphism nor cumulativity. It should be fast, with hashconsing;
-  and simple enough (no inductives, no universe trickery).
+    The core terms are expressions in the calculus of constructions, with no
+    universe polymorphism nor cumulativity. It should be fast, with hashconsing;
+    and simple enough (no inductives, no universe trickery).
 
-  It is intended to be the foundation for user-level terms and types and formulas.
-*)
+    It is intended to be the foundation for user-level terms and types and
+    formulas. *)
 
 open Types_
 
@@ -41,9 +41,9 @@ val as_type : t -> Level.t option
 val as_type_exn : t -> Level.t
 
 val iter_shallow : f:(bool -> t -> unit) -> t -> unit
-(** [iter_shallow f e] iterates on immediate subterms of [e],
-    calling [f trdb e'] for each subterm [e'], with [trdb = true] iff
-    [e'] is directly under a binder. *)
+(** [iter_shallow f e] iterates on immediate subterms of [e], calling
+    [f trdb e'] for each subterm [e'], with [trdb = true] iff [e'] is directly
+    under a binder. *)
 
 val map_shallow : f:(bool -> t -> t) -> t -> t
 val exists_shallow : f:(bool -> t -> bool) -> t -> bool
@@ -53,8 +53,8 @@ val is_type : t -> bool
 (** [is_type t] is true iff [view t] is [Type _] *)
 
 val is_closed : t -> bool
-(** Is the term closed (all bound variables are paired with a binder)?
- time: O(1) *)
+(** Is the term closed (all bound variables are paired with a binder)? time:
+    O(1) *)
 
 (** {2 Creation} *)
 
@@ -75,8 +75,8 @@ val subst_level : Level.subst -> t -> t
 (** De bruijn indices *)
 module DB : sig
   val subst_db0 : t -> by:t -> t
-  (** [subst_db0 store t ~by] replaces bound variable 0 in [t] with
-      the term [by]. This is useful, for example, to implement beta-reduction.
+  (** [subst_db0 store t ~by] replaces bound variable 0 in [t] with the term
+      [by]. This is useful, for example, to implement beta-reduction.
 
       For example, with [t] being [_[0] = (\x. _[2] _[1] x[0])],
       [subst_db0 store t ~by:"hello"] is ["hello" = (\x. _[2] "hello" x[0])]. *)
@@ -84,9 +84,9 @@ module DB : sig
   val subst_db_l : t -> t list -> t
 
   val shift : t -> by:int -> t
-  (** [shift t ~by] shifts all bound variables in [t] that are not
-      closed on, by amount [by] (which must be >= 0).
+  (** [shift t ~by] shifts all bound variables in [t] that are not closed on, by
+      amount [by] (which must be >= 0).
 
-      For example, with term [t] being [\x. _[1] _[2] x[0]],
-      [shift t ~by:5] is [\x. _[6] _[7] x[0]]. *)
+      For example, with term [t] being [\x. _[1] _[2] x[0]], [shift t ~by:5] is
+      [\x. _[6] _[7] x[0]]. *)
 end