Merge PR #11251: [micromega] reformating using ocamlformat

Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes

1 files changed, 357 insertions, 464 deletions

diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 0a57677220..5d8ae83853 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -27,10 +27,7 @@ let pr_constr env evd e = Printer.pr_econstr_env env evd e
 let rec find_option pred l =
   match l with
   | [] -> raise Not_found
-  | e::l -> match pred e with
-            | Some r -> r
-            | None   -> find_option pred l
-
+  | e :: l -> ( match pred e with Some r -> r | None -> find_option pred l )
 
 (** [HConstr] is a map indexed by EConstr.t.
     It should only be used using closed terms.
@@ -39,8 +36,7 @@ module HConstr = struct
   module M = Map.Make (struct
     type t = EConstr.t
 
-    let compare c c' =
-      Constr.compare (unsafe_to_constr c) (unsafe_to_constr c')
+    let compare c c' = Constr.compare (unsafe_to_constr c) (unsafe_to_constr c')
   end)
 
   type 'a t = 'a list M.t
@@ -52,91 +48,89 @@ module HConstr = struct
     M.add h (e :: l) m
 
   let empty = M.empty
-
   let find h m = match lfind h m with e :: _ -> e | [] -> raise Not_found
-
   let find_all = lfind
 
   let fold f m acc =
     M.fold (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l) m acc
-
 end
 
-
 (** [get_projections_from_constant (evd,c) ]
     returns an array of constr [| a1,.. an|] such that [c] is defined as
     Definition c := mk a1 .. an with mk a constructor.
     ai is therefore either a type parameter or a projection.
  *)
 
-
 let get_projections_from_constant (evd, i) =
-  match EConstr.kind evd (Reductionops.clos_whd_flags CClosure.all (Global.env ()) evd i) with
+  match
+    EConstr.kind evd
+      (Reductionops.clos_whd_flags CClosure.all (Global.env ()) evd i)
+  with
   | App (c, a) -> Some a
   | _ ->
-     raise (CErrors.user_err Pp.(str "The hnf of term " ++ pr_constr (Global.env ()) evd i
-                          ++ str " should be an application i.e. (c a1 ... an)"))
+    raise
+      (CErrors.user_err
+         Pp.(
+           str "The hnf of term "
+           ++ pr_constr (Global.env ()) evd i
+           ++ str " should be an application i.e. (c a1 ... an)"))
 
 (**  An instance of type, say T, is registered into a hashtable, say TableT. *)
 
 type 'a decl =
-  { decl: EConstr.t
+  { decl : EConstr.t
   ; (* Registered type instance *)
-    deriv: 'a
-  (* Projections of insterest *) }
-
+    deriv : 'a (* Projections of insterest *) }
 
 module EInjT = struct
   type t =
-    { isid: bool
+    { isid : bool
     ; (* S = T ->  inj = fun x -> x*)
-      source: EConstr.t
+      source : EConstr.t
     ; (* S *)
-      target: EConstr.t
+      target : EConstr.t
     ; (* T *)
       (* projections *)
-      inj: EConstr.t
+      inj : EConstr.t
     ; (* S -> T *)
-      pred: EConstr.t
+      pred : EConstr.t
     ; (* T -> Prop *)
-      cstr: EConstr.t option
-    (* forall x, pred (inj x) *) }
+      cstr : EConstr.t option (* forall x, pred (inj x) *) }
 end
 
 module EBinOpT = struct
   type t =
     { (* Op : source1 -> source2 -> source3 *)
-      source1: EConstr.t
-    ; source2: EConstr.t
-    ; source3: EConstr.t
-    ; target: EConstr.t
-    ; inj1: EConstr.t
+      source1 : EConstr.t
+    ; source2 : EConstr.t
+    ; source3 : EConstr.t
+    ; target : EConstr.t
+    ; inj1 : EConstr.t
     ; (* InjTyp source1 target *)
-      inj2: EConstr.t
+      inj2 : EConstr.t
     ; (* InjTyp source2 target *)
-      inj3: EConstr.t
+      inj3 : EConstr.t
     ; (* InjTyp source3 target *)
-      tbop: EConstr.t
-    (* TBOpInj *) }
+      tbop : EConstr.t (* TBOpInj *) }
 end
 
 module ECstOpT = struct
-  type t = {source: EConstr.t; target: EConstr.t; inj: EConstr.t}
+  type t = {source : EConstr.t; target : EConstr.t; inj : EConstr.t}
 end
 
 module EUnOpT = struct
   type t =
-    { source1: EConstr.t
-    ; source2: EConstr.t
-    ; target: EConstr.t
-    ; inj1_t: EConstr.t
-    ; inj2_t: EConstr.t
-    ; unop: EConstr.t }
+    { source1 : EConstr.t
+    ; source2 : EConstr.t
+    ; target : EConstr.t
+    ; inj1_t : EConstr.t
+    ; inj2_t : EConstr.t
+    ; unop : EConstr.t }
 end
 
 module EBinRelT = struct
   type t =
-    {source: EConstr.t; target: EConstr.t; inj: EConstr.t; brel: EConstr.t}
+    {source : EConstr.t; target : EConstr.t; inj : EConstr.t; brel : EConstr.t}
 end
 
 module EPropBinOpT = struct
@@ -147,37 +141,32 @@ module EPropUnOpT = struct
   type t = EConstr.t
 end
 
-
 module ESatT = struct
-  type t =  {parg1: EConstr.t; parg2: EConstr.t; satOK: EConstr.t}
+  type t = {parg1 : EConstr.t; parg2 : EConstr.t; satOK : EConstr.t}
 end
 
 (* Different type of declarations *)
 type decl_kind =
   | PropOp of EPropBinOpT.t decl
-  | PropUnOp  of EPropUnOpT.t decl
-  | InjTyp of EInjT.t  decl
-  | BinRel of EBinRelT.t  decl
-  | BinOp  of EBinOpT.t  decl
-  | UnOp   of EUnOpT.t  decl
-  | CstOp  of ECstOpT.t  decl
-  | Saturate of ESatT.t  decl
-
-
-let get_decl  = function
+  | PropUnOp of EPropUnOpT.t decl
+  | InjTyp of EInjT.t decl
+  | BinRel of EBinRelT.t decl
+  | BinOp of EBinOpT.t decl
+  | UnOp of EUnOpT.t decl
+  | CstOp of ECstOpT.t decl
+  | Saturate of ESatT.t decl
+
+let get_decl = function
   | PropOp d -> d.decl
-  | PropUnOp  d -> d.decl
-  | InjTyp d    -> d.decl
-  | BinRel d    -> d.decl
-  | BinOp  d    -> d.decl
-  | UnOp   d    -> d.decl
-  | CstOp  d    -> d.decl
-  | Saturate d  -> d.decl
-
-type term_kind =
-  | Application of EConstr.constr
-  | OtherTerm of EConstr.constr
+  | PropUnOp d -> d.decl
+  | InjTyp d -> d.decl
+  | BinRel d -> d.decl
+  | BinOp d -> d.decl
+  | UnOp d -> d.decl
+  | CstOp d -> d.decl
+  | Saturate d -> d.decl
 
+type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr
 
 module type Elt = sig
   type elt
@@ -185,11 +174,9 @@ module type Elt = sig
   val name : string
   (** name *)
 
-  val table : (term_kind * decl_kind)  HConstr.t ref
-
+  val table : (term_kind * decl_kind) HConstr.t ref
   val cast : elt decl -> decl_kind
-
-  val dest : decl_kind -> (elt decl) option
+  val dest : decl_kind -> elt decl option
 
   val get_key : int
   (** [get_key] is the type-index used as key for the instance *)
@@ -199,19 +186,14 @@ module type Elt = sig
         built from the type-instance i and the arguments (type indexes and projections)
         of the type-class constructor. *)
 
-                                                                 (*  val arity : int*)
-
+  (*  val arity : int*)
 end
 
-
-let table =  Summary.ref  ~name:("zify_table") HConstr.empty
-
-let saturate = Summary.ref ~name:("zify_saturate") HConstr.empty
-
+let table = Summary.ref ~name:"zify_table" HConstr.empty
+let saturate = Summary.ref ~name:"zify_saturate" HConstr.empty
 let table_cache = ref HConstr.empty
 let saturate_cache = ref HConstr.empty
 
-
 (** Each type-class gives rise to a different table.
     They only differ on how projections are extracted.  *)
 module EInj = struct
@@ -220,186 +202,129 @@ module EInj = struct
   type elt = EInjT.t
 
   let name = "EInj"
-
   let table = table
-
   let cast x = InjTyp x
-
-  let dest = function
-    | InjTyp x -> Some x
-    | _        -> None
-
+  let dest = function InjTyp x -> Some x | _ -> None
 
   let mk_elt evd i (a : EConstr.t array) =
     let isid = EConstr.eq_constr evd a.(0) a.(1) in
     { isid
-    ; source= a.(0)
-    ; target= a.(1)
-    ; inj= a.(2)
-    ; pred= a.(3)
-    ; cstr= (if isid then None else Some a.(4)) }
+    ; source = a.(0)
+    ; target = a.(1)
+    ; inj = a.(2)
+    ; pred = a.(3)
+    ; cstr = (if isid then None else Some a.(4)) }
 
   let get_key = 0
-
 end
 
 module EBinOp = struct
   type elt = EBinOpT.t
+
   open EBinOpT
 
   let name = "BinOp"
-
   let table = table
 
   let mk_elt evd i a =
-    { source1= a.(0)
-    ; source2= a.(1)
-    ; source3= a.(2)
-    ; target= a.(3)
-    ; inj1= a.(5)
-    ; inj2= a.(6)
-    ; inj3= a.(7)
-    ; tbop= a.(9) }
+    { source1 = a.(0)
+    ; source2 = a.(1)
+    ; source3 = a.(2)
+    ; target = a.(3)
+    ; inj1 = a.(5)
+    ; inj2 = a.(6)
+    ; inj3 = a.(7)
+    ; tbop = a.(9) }
 
   let get_key = 4
-
-
   let cast x = BinOp x
-
-  let dest = function
-    | BinOp  x -> Some x
-    | _  -> None
-
+  let dest = function BinOp x -> Some x | _ -> None
 end
 
 module ECstOp = struct
   type elt = ECstOpT.t
+
   open ECstOpT
 
   let name = "CstOp"
-
   let table = table
-
   let cast x = CstOp x
-
-  let dest = function
-    | CstOp  x -> Some x
-    | _  -> None
-
-
-  let mk_elt evd i a = {source= a.(0); target= a.(1); inj= a.(3)}
-
+  let dest = function CstOp x -> Some x | _ -> None
+  let mk_elt evd i a = {source = a.(0); target = a.(1); inj = a.(3)}
   let get_key = 2
-
 end
 
 module EUnOp = struct
   type elt = EUnOpT.t
+
   open EUnOpT
 
   let name = "UnOp"
-
   let table = table
-
   let cast x = UnOp x
-
-  let dest = function
-    | UnOp  x -> Some x
-    | _  -> None
-
+  let dest = function UnOp x -> Some x | _ -> None
 
   let mk_elt evd i a =
-    { source1= a.(0)
-    ; source2= a.(1)
-    ; target= a.(2)
-    ; inj1_t= a.(4)
-    ; inj2_t= a.(5)
-    ; unop= a.(6) }
+    { source1 = a.(0)
+    ; source2 = a.(1)
+    ; target = a.(2)
+    ; inj1_t = a.(4)
+    ; inj2_t = a.(5)
+    ; unop = a.(6) }
 
   let get_key = 3
-
 end
 
 module EBinRel = struct
   type elt = EBinRelT.t
+
   open EBinRelT
 
   let name = "BinRel"
-
   let table = table
-
   let cast x = BinRel x
+  let dest = function BinRel x -> Some x | _ -> None
 
-  let dest = function
-    | BinRel  x -> Some x
-    | _  -> None
-
-  let mk_elt evd i a = {source= a.(0); target= a.(1); inj= a.(3); brel= a.(4)}
+  let mk_elt evd i a =
+    {source = a.(0); target = a.(1); inj = a.(3); brel = a.(4)}
 
   let get_key = 2
-
 end
 
 module EPropOp = struct
   type elt = EConstr.t
 
   let name = "PropBinOp"
-
   let table = table
-
   let cast x = PropOp x
-
-  let dest = function
-    | PropOp  x -> Some x
-    | _  -> None
-
+  let dest = function PropOp x -> Some x | _ -> None
   let mk_elt evd i a = i
-
   let get_key = 0
-
 end
 
 module EPropUnOp = struct
   type elt = EConstr.t
 
   let name = "PropUnOp"
-
   let table = table
-
   let cast x = PropUnOp x
-
-  let dest = function
-    | PropUnOp  x -> Some x
-    | _  -> None
-
+  let dest = function PropUnOp x -> Some x | _ -> None
   let mk_elt evd i a = i
-
   let get_key = 0
-
 end
 
-
-
-let constr_of_term_kind = function
-  | Application c -> c
-  | OtherTerm   c -> c
-
-
+let constr_of_term_kind = function Application c -> c | OtherTerm c -> c
 
 let fold_declared_const f evd acc =
   HConstr.fold
-    (fun _ (_,e) acc -> f (fst (EConstr.destConst evd (get_decl e))) acc)
-    (!table_cache) acc
-
-
+    (fun _ (_, e) acc -> f (fst (EConstr.destConst evd (get_decl e))) acc)
+    !table_cache acc
 
 module type S = sig
   val register : Constrexpr.constr_expr -> unit
-
   val print : unit -> unit
 end
 
-
 module MakeTable (E : Elt) = struct
   (** Given a term [c] and its arguments ai,
         we construct a HConstr.t table that is
@@ -410,33 +335,34 @@ module MakeTable (E : Elt) = struct
   let make_elt (evd, i) =
     match get_projections_from_constant (evd, i) with
     | None ->
-        let env = Global.env () in
-        let t = string_of_ppcmds (pr_constr env evd i) in
-        failwith ("Cannot register term " ^ t)
+      let env = Global.env () in
+      let t = string_of_ppcmds (pr_constr env evd i) in
+      failwith ("Cannot register term " ^ t)
     | Some a -> E.mk_elt evd i a
 
-  let register_hint  evd t elt =
+  let register_hint evd t elt =
     match EConstr.kind evd t with
-    | App(c,_) ->
-       E.table := HConstr.add c (Application t, E.cast elt) !E.table
-    |  _       -> E.table := HConstr.add t (OtherTerm t, E.cast elt) !E.table
-
-
-
+    | App (c, _) ->
+      E.table := HConstr.add c (Application t, E.cast elt) !E.table
+    | _ -> E.table := HConstr.add t (OtherTerm t, E.cast elt) !E.table
 
   let register_constr env evd c =
     let c = EConstr.of_constr c in
     let t = get_type_of env evd c in
     match EConstr.kind evd t with
     | App (intyp, args) ->
-        let styp = args.(E.get_key) in
-        let elt = {decl= c; deriv=  (make_elt (evd, c))} in
-        register_hint evd styp elt
+      let styp = args.(E.get_key) in
+      let elt = {decl = c; deriv = make_elt (evd, c)} in
+      register_hint evd styp elt
     | _ ->
-       let env = Global.env () in
-       raise (CErrors.user_err Pp.
-              (str ": Cannot register term "++pr_constr env evd c++
-                 str ". It has type "++pr_constr env evd t++str " which should be of the form  [F X1 .. Xn]"))
+      let env = Global.env () in
+      raise
+        (CErrors.user_err
+           Pp.(
+             str ": Cannot register term "
+             ++ pr_constr env evd c ++ str ". It has type "
+             ++ pr_constr env evd t
+             ++ str " which should be of the form  [F X1 .. Xn]"))
 
   let register_obj : Constr.constr -> Libobject.obj =
     let cache_constr (_, c) =
@@ -447,7 +373,7 @@ module MakeTable (E : Elt) = struct
     let subst_constr (subst, c) = Mod_subst.subst_mps subst c in
     Libobject.declare_object
     @@ Libobject.superglobal_object_nodischarge
-         ("register-zify-" ^  E.name)
+         ("register-zify-" ^ E.name)
          ~cache:cache_constr ~subst:(Some subst_constr)
 
   (** [register c] is called from the VERNACULAR ADD [name] constr(t).
@@ -455,52 +381,40 @@ module MakeTable (E : Elt) = struct
        registered as a [superglobal_object_nodischarge].
        TODO: pre-compute [get_type_of] - [cache_constr] is using another environment.
      *)
-  let register = fun c ->
+  let register c =
     let env = Global.env () in
     let evd = Evd.from_env env in
     let evd, c = Constrintern.interp_open_constr env evd c in
     let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in
     ()
 
-
   let pp_keys () =
     let env = Global.env () in
     let evd = Evd.from_env env in
     HConstr.fold
-      (fun _ (k,d) acc ->
+      (fun _ (k, d) acc ->
         match E.dest d with
         | None -> acc
         | Some _ ->
-           Pp.(pr_constr env evd (constr_of_term_kind k) ++ str " " ++ acc))
-      (!E.table) (Pp.str "")
-
-
-  let print () =  Feedback.msg_info (pp_keys ())
+          Pp.(pr_constr env evd (constr_of_term_kind k) ++ str " " ++ acc))
+      !E.table (Pp.str "")
 
+  let print () = Feedback.msg_info (pp_keys ())
 end
 
-
 module InjTable = MakeTable (EInj)
 
-
 module ESat = struct
   type elt = ESatT.t
+
   open ESatT
 
   let name = "Saturate"
-
   let table = saturate
-
   let cast x = Saturate x
-
-  let dest = function
-    | Saturate  x -> Some x
-    | _  -> None
-
-  let mk_elt evd i a = {parg1= a.(2); parg2= a.(3); satOK= a.(5)}
-
+  let dest = function Saturate x -> Some x | _ -> None
+  let mk_elt evd i a = {parg1 = a.(2); parg2 = a.(3); satOK = a.(5)}
   let get_key = 1
-
 end
 
 module BinOp = MakeTable (EBinOp)
@@ -512,10 +426,9 @@ module PropUnOp = MakeTable (EPropUnOp)
 module Saturate = MakeTable (ESat)
 
 let init_cache () =
-  table_cache :=  !table;
+  table_cache := !table;
   saturate_cache := !saturate
 
-
 (** The module [Spec] is used to register
     the instances of [BinOpSpec], [UnOpSpec].
     They are not indexed and stored in a list. *)
@@ -556,7 +469,6 @@ module Spec = struct
     Feedback.msg_notice l
 end
 
-
 let unfold_decl evd =
   let f cst acc = cst :: acc in
   fold_declared_const f evd []
@@ -578,33 +490,19 @@ let locate_const str =
 
 (* The following [constr] are necessary for constructing the proof terms *)
 let mkapp2 = lazy (zify "mkapp2")
-
 let mkapp = lazy (zify "mkapp")
-
 let mkapp0 = lazy (zify "mkapp0")
-
 let mkdp = lazy (zify "mkinjterm")
-
 let eq_refl = lazy (zify "eq_refl")
-
 let mkrel = lazy (zify "mkrel")
-
 let mkprop_op = lazy (zify "mkprop_op")
-
 let mkuprop_op = lazy (zify "mkuprop_op")
-
 let mkdpP = lazy (zify "mkinjprop")
-
 let iff_refl = lazy (zify "iff_refl")
-
 let q = lazy (zify "target_prop")
-
 let ieq = lazy (zify "injprop_ok")
-
 let iff = lazy (zify "iff")
 
-
-
 (* A super-set of the previous are needed to unfold the generated proof terms. *)
 
 let to_unfold =
@@ -631,7 +529,6 @@ let to_unfold =
        ; "mkapp0"
        ; "mkprop_op" ])
 
-
 (** Module [CstrTable] records terms  [x] injected into [inj x]
     together with the corresponding type constraint.
     The terms are stored by side-effect during the traversal
@@ -644,17 +541,15 @@ module CstrTable = struct
     type t = EConstr.t
 
     let hash c = Constr.hash (unsafe_to_constr c)
-
     let equal c c' = Constr.equal (unsafe_to_constr c) (unsafe_to_constr c')
   end)
 
   let table : EConstr.t HConstr.t = HConstr.create 10
-
   let register evd t (i : EConstr.t) = HConstr.add table t i
 
   let get () =
     let l = HConstr.fold (fun k i acc -> (k, i) :: acc) table [] in
-    HConstr.clear table ; l
+    HConstr.clear table; l
 
   (** [gen_cstr table] asserts (cstr k) for each element of the table (k,cstr).
         NB: the constraint is only asserted if it does not already exist in the context.
@@ -667,7 +562,7 @@ module CstrTable = struct
           let hyps_table = HConstr.create 20 in
           List.iter
             (fun (_, (t : EConstr.types)) -> HConstr.add hyps_table t ())
-            (Tacmach.New.pf_hyps_types gl) ;
+            (Tacmach.New.pf_hyps_types gl);
           fun c -> HConstr.mem hyps_table c
         in
         (* Add the constraint (cstr k) if it is not already present *)
@@ -683,17 +578,16 @@ module CstrTable = struct
                     (Names.Id.of_string "cstr")
                     env
                 in
-                Tactics.pose_proof (Names.Name n) term )
+                Tactics.pose_proof (Names.Name n) term)
         in
         List.fold_left
           (fun acc (k, i) -> Tacticals.New.tclTHEN (gen k i) acc)
-          Tacticals.New.tclIDTAC table )
+          Tacticals.New.tclIDTAC table)
 end
 
 let mkvar red evd inj v =
   ( if not red then
-    match inj.cstr with None -> () | Some ctr -> CstrTable.register evd v ctr
-  ) ;
+    match inj.cstr with None -> () | Some ctr -> CstrTable.register evd v ctr );
   let iv = EConstr.mkApp (inj.inj, [|v|]) in
   let iv = if red then Tacred.compute (Global.env ()) evd iv else iv in
   EConstr.mkApp
@@ -724,11 +618,8 @@ let inj_term_of_texpr evd = function
   | Var (inj, e) -> mkvar false evd inj e
   | Constant (inj, e) -> mkvar true evd inj e
 
-let mkapp2_id evd i (* InjTyp S3 T *)
-                    inj (* deriv i *)
-                        t (* S1 -> S2 -> S3 *)
-                          b (* Binop S1 S2 S3 t ... *)
-                            dbop (* deriv b *) e1 e2 =
+let mkapp2_id evd i (* InjTyp S3 T *) inj (* deriv i *) t (* S1 -> S2 -> S3 *) b
+    (* Binop S1 S2 S3 t ... *) dbop (* deriv b *) e1 e2 =
   let default () =
     let e1' = inj_term_of_texpr evd e1 in
     let e2' = inj_term_of_texpr evd e2 in
@@ -755,15 +646,16 @@ let mkapp2_id evd i (* InjTyp S3 T *)
      |Var (_, e1), Var (_, e2)
      |Constant (_, e1), Var (_, e2)
      |Var (_, e1), Constant (_, e2) ->
-        Var (inj, EConstr.mkApp (t, [|e1; e2|]))
+      Var (inj, EConstr.mkApp (t, [|e1; e2|]))
     | _, _ -> default ()
 
 let mkapp_id evd i inj (unop, u) f e1 =
-  EUnOpT.(if EConstr.eq_constr evd u.unop f then
-    (* Injection does nothing *)
-    match e1 with
-    | Constant (_, e) | Var (_, e) -> Var (inj, EConstr.mkApp (f, [|e|]))
-    | Injterm e1 ->
+  EUnOpT.(
+    if EConstr.eq_constr evd u.unop f then
+      (* Injection does nothing *)
+      match e1 with
+      | Constant (_, e) | Var (_, e) -> Var (inj, EConstr.mkApp (f, [|e|]))
+      | Injterm e1 ->
         Injterm
           (EConstr.mkApp
              ( force mkapp
@@ -775,124 +667,128 @@ let mkapp_id evd i inj (unop, u) f e1 =
                 ; u.inj2_t
                 ; unop
                 ; e1 |] ))
-  else
-    let e1 = inj_term_of_texpr evd e1 in
-    Injterm
-      (EConstr.mkApp
-         ( force mkapp
-         , [|u.source1; u.source2; u.target; f; u.inj1_t; u.inj2_t; unop; e1|]
-         )))
-
-type typed_constr = {constr: EConstr.t; typ: EConstr.t}
-
+    else
+      let e1 = inj_term_of_texpr evd e1 in
+      Injterm
+        (EConstr.mkApp
+           ( force mkapp
+           , [|u.source1; u.source2; u.target; f; u.inj1_t; u.inj2_t; unop; e1|]
+           )))
 
+type typed_constr = {constr : EConstr.t; typ : EConstr.t}
 
 let get_injection env evd t =
   match snd (HConstr.find t !table_cache) with
   | InjTyp i -> i
-  | _        -> raise Not_found
-
-
- (* [arrow] is the term (fun (x:Prop) (y : Prop) => x -> y) *)
- let arrow =
-   let name x =
-     Context.make_annot (Name.mk_name (Names.Id.of_string x)) Sorts.Relevant  in
-   EConstr.mkLambda
-     ( name "x"
-     , EConstr.mkProp
-     , EConstr.mkLambda
-         ( name "y"
-         , EConstr.mkProp
-         , EConstr.mkProd
-             ( Context.make_annot Names.Anonymous Sorts.Relevant
-             , EConstr.mkRel 2
-             , EConstr.mkRel 2 ) ) )
-
-
- let is_prop env sigma term =
-  let sort  = Retyping.get_sort_of env sigma term in
+  | _ -> raise Not_found
+
+(* [arrow] is the term (fun (x:Prop) (y : Prop) => x -> y) *)
+let arrow =
+  let name x =
+    Context.make_annot (Name.mk_name (Names.Id.of_string x)) Sorts.Relevant
+  in
+  EConstr.mkLambda
+    ( name "x"
+    , EConstr.mkProp
+    , EConstr.mkLambda
+        ( name "y"
+        , EConstr.mkProp
+        , EConstr.mkProd
+            ( Context.make_annot Names.Anonymous Sorts.Relevant
+            , EConstr.mkRel 2
+            , EConstr.mkRel 2 ) ) )
+
+let is_prop env sigma term =
+  let sort = Retyping.get_sort_of env sigma term in
   Sorts.is_prop sort
 
- (** [get_application env evd e] expresses [e] as an application (c a)
+(** [get_application env evd e] expresses [e] as an application (c a)
      where c is the head symbol and [a] is the array of arguments.
      The function also transforms (x -> y) as (arrow x y) *)
- let get_operator env evd e =
-   let is_arrow a p1 p2 =
-     is_prop env evd p1 && is_prop (EConstr.push_rel (Context.Rel.Declaration.LocalAssum(a,p1)) env) evd p2
-     && (a.Context.binder_name = Names.Anonymous || EConstr.Vars.noccurn evd 1 p2) in
-   match EConstr.kind evd e with
-   | Prod (a, p1, p2) when is_arrow a p1 p2 ->
-      (arrow,[|p1 ;p2|])
-   | App(c,a) -> (c,a)
-   |  _       -> (e,[||])
-
+let get_operator env evd e =
+  let is_arrow a p1 p2 =
+    is_prop env evd p1
+    && is_prop
+         (EConstr.push_rel (Context.Rel.Declaration.LocalAssum (a, p1)) env)
+         evd p2
+    && (a.Context.binder_name = Names.Anonymous || EConstr.Vars.noccurn evd 1 p2)
+  in
+  match EConstr.kind evd e with
+  | Prod (a, p1, p2) when is_arrow a p1 p2 -> (arrow, [|p1; p2|])
+  | App (c, a) -> (c, a)
+  | _ -> (e, [||])
 
- let is_convertible env evd k t =
-   Reductionops.check_conv env evd k t
+let is_convertible env evd k t = Reductionops.check_conv env evd k t
 
- (** [match_operator env evd hd arg (t,d)]
+(** [match_operator env evd hd arg (t,d)]
      - hd is head operator of t
      - If t = OtherTerm _, then t = hd
      - If t = Application _, then
        we extract the relevant number of arguments from arg
        and check for convertibility *)
- let match_operator env evd hd args (t, d) =
-   let decomp t i =
-     let n = Array.length args in
-     let t' = EConstr.mkApp(hd,Array.sub args 0 (n-i)) in
-          if is_convertible env evd t' t
-          then Some (d,t)
-          else None in
-
-   match t with
-   | OtherTerm t -> Some(d,t)
-   | Application t ->
-      match d with
-      | CstOp _    -> decomp t 0
-      | UnOp _     -> decomp t 1
-      | BinOp _    -> decomp t 2
-      | BinRel _   -> decomp t 2
-      | PropOp _   -> decomp t 2
-      | PropUnOp _ -> decomp t 1
-      |  _  -> None
-
-
- let rec trans_expr env evd e =
+let match_operator env evd hd args (t, d) =
+  let decomp t i =
+    let n = Array.length args in
+    let t' = EConstr.mkApp (hd, Array.sub args 0 (n - i)) in
+    if is_convertible env evd t' t then Some (d, t) else None
+  in
+  match t with
+  | OtherTerm t -> Some (d, t)
+  | Application t -> (
+    match d with
+    | CstOp _ -> decomp t 0
+    | UnOp _ -> decomp t 1
+    | BinOp _ -> decomp t 2
+    | BinRel _ -> decomp t 2
+    | PropOp _ -> decomp t 2
+    | PropUnOp _ -> decomp t 1
+    | _ -> None )
+
+let rec trans_expr env evd e =
   (* Get the injection *)
-  let {decl= i; deriv= inj} = get_injection  env evd e.typ in
+  let {decl = i; deriv = inj} = get_injection env evd e.typ in
   let e = e.constr in
   if EConstr.isConstruct evd e then Constant (inj, e) (* Evaluate later *)
   else
-    let (c,a) = get_operator env evd e in
+    let c, a = get_operator env evd e in
     try
-      let (k,t) = find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) in
+      let k, t =
+        find_option
+          (match_operator env evd c a)
+          (HConstr.find_all c !table_cache)
+      in
       let n = Array.length a in
-       match k with
-       | CstOp {decl = c'} ->
-          Injterm (EConstr.mkApp (force mkapp0, [|inj.source; inj.target; e; i; c'|]))
-       | UnOp {decl = unop ; deriv = u} ->
-          let a' = trans_expr env evd {constr= a.(n-1); typ= u.EUnOpT.source1} in
-            if is_constant a' && EConstr.isConstruct evd t then
-              Constant (inj, e)
-            else mkapp_id evd i inj (unop, u) t a'
-       | BinOp {decl = binop ; deriv = b} ->
-          let a0 = trans_expr env evd {constr= a.(n-2); typ= b.EBinOpT.source1} in
-          let a1 = trans_expr env evd {constr= a.(n-1); typ= b.EBinOpT.source2} in
-          if is_constant a0 && is_constant a1 && EConstr.isConstruct evd t
-          then Constant (inj, e)
-          else mkapp2_id evd i inj t binop b a0 a1
-       |  d  ->
-           Var (inj,e)
-    with Not_found -> Var (inj,e)
+      match k with
+      | CstOp {decl = c'} ->
+        Injterm
+          (EConstr.mkApp (force mkapp0, [|inj.source; inj.target; e; i; c'|]))
+      | UnOp {decl = unop; deriv = u} ->
+        let a' =
+          trans_expr env evd {constr = a.(n - 1); typ = u.EUnOpT.source1}
+        in
+        if is_constant a' && EConstr.isConstruct evd t then Constant (inj, e)
+        else mkapp_id evd i inj (unop, u) t a'
+      | BinOp {decl = binop; deriv = b} ->
+        let a0 =
+          trans_expr env evd {constr = a.(n - 2); typ = b.EBinOpT.source1}
+        in
+        let a1 =
+          trans_expr env evd {constr = a.(n - 1); typ = b.EBinOpT.source2}
+        in
+        if is_constant a0 && is_constant a1 && EConstr.isConstruct evd t then
+          Constant (inj, e)
+        else mkapp2_id evd i inj t binop b a0 a1
+      | d -> Var (inj, e)
+    with Not_found -> Var (inj, e)
 
 let trans_expr env evd e =
-  try trans_expr env evd e with Not_found ->
+  try trans_expr env evd e
+  with Not_found ->
     raise
       (CErrors.user_err
          ( Pp.str "Missing injection for type "
          ++ Printer.pr_leconstr_env env evd e.typ ))
 
-
 type tprop =
   | TProp of EConstr.t  (** Transformed proposition *)
   | IProp of EConstr.t  (** Identical proposition *)
@@ -903,72 +799,72 @@ let mk_iprop e =
 let inj_prop_of_tprop = function TProp p -> p | IProp e -> mk_iprop e
 
 let rec trans_prop env evd e =
-  let (c,a) = get_operator env evd e in
+  let c, a = get_operator env evd e in
   try
-    let (k,t) = find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) in
+    let k, t =
+      find_option (match_operator env evd c a) (HConstr.find_all c !table_cache)
+    in
     let n = Array.length a in
     match k with
-    | PropOp {decl= rop} ->
-       begin
-         try
-           let t1 = trans_prop env evd a.(n-2) in
-           let t2 = trans_prop env evd a.(n-1) in
-           match (t1, t2) with
-            | IProp _, IProp _ -> IProp e
-            | _, _ ->
-               let t1 = inj_prop_of_tprop t1 in
-                let t2 = inj_prop_of_tprop t2 in
-                TProp (EConstr.mkApp (force mkprop_op, [|t; rop; t1; t2|]))
-         with Not_found -> IProp e
-       end
-    | BinRel {decl = br ; deriv = rop} ->
-       begin
-       try
-            let a1 = trans_expr env evd {constr = a.(n-2) ; typ = rop.EBinRelT.source} in
-            let a2 = trans_expr env evd {constr = a.(n-1) ; typ = rop.EBinRelT.source} in
-            if EConstr.eq_constr evd t rop.EBinRelT.brel then
-              match (constr_of_texpr a1, constr_of_texpr a2) with
-              | Some e1, Some e2 -> IProp (EConstr.mkApp (t, [|e1; e2|]))
-              | _, _ ->
-                  let a1 = inj_term_of_texpr evd a1 in
-                  let a2 = inj_term_of_texpr evd a2 in
-                  TProp
-                    (EConstr.mkApp
-                       ( force mkrel
-                       , [| rop.EBinRelT.source
-                          ; rop.EBinRelT.target
-                          ; t
-                          ; rop.EBinRelT.inj
-                          ; br
-                          ; a1
-                          ; a2 |] ))
-            else
-              let a1 = inj_term_of_texpr evd a1 in
-              let a2 = inj_term_of_texpr evd a2 in
-              TProp
-                (EConstr.mkApp
-                   ( force mkrel
-                   , [| rop.EBinRelT.source
-                      ; rop.EBinRelT.target
-                      ; t
-                      ; rop.EBinRelT.inj
-                      ; br
-                      ; a1
-                      ; a2 |] ))
-          with Not_found -> IProp e
-       end
-    | PropUnOp {decl = rop} ->
-     begin
-       try
-         let t1 = trans_prop env evd a.(n-1) in
-         match t1 with
-         | IProp _ -> IProp e
-         | _ ->
-            let t1 = inj_prop_of_tprop t1 in
-              TProp (EConstr.mkApp (force mkuprop_op, [|t; rop; t1|]))
-       with Not_found -> IProp e
-     end
-  | _ ->  IProp e
+    | PropOp {decl = rop} -> (
+      try
+        let t1 = trans_prop env evd a.(n - 2) in
+        let t2 = trans_prop env evd a.(n - 1) in
+        match (t1, t2) with
+        | IProp _, IProp _ -> IProp e
+        | _, _ ->
+          let t1 = inj_prop_of_tprop t1 in
+          let t2 = inj_prop_of_tprop t2 in
+          TProp (EConstr.mkApp (force mkprop_op, [|t; rop; t1; t2|]))
+      with Not_found -> IProp e )
+    | BinRel {decl = br; deriv = rop} -> (
+      try
+        let a1 =
+          trans_expr env evd {constr = a.(n - 2); typ = rop.EBinRelT.source}
+        in
+        let a2 =
+          trans_expr env evd {constr = a.(n - 1); typ = rop.EBinRelT.source}
+        in
+        if EConstr.eq_constr evd t rop.EBinRelT.brel then
+          match (constr_of_texpr a1, constr_of_texpr a2) with
+          | Some e1, Some e2 -> IProp (EConstr.mkApp (t, [|e1; e2|]))
+          | _, _ ->
+            let a1 = inj_term_of_texpr evd a1 in
+            let a2 = inj_term_of_texpr evd a2 in
+            TProp
+              (EConstr.mkApp
+                 ( force mkrel
+                 , [| rop.EBinRelT.source
+                    ; rop.EBinRelT.target
+                    ; t
+                    ; rop.EBinRelT.inj
+                    ; br
+                    ; a1
+                    ; a2 |] ))
+        else
+          let a1 = inj_term_of_texpr evd a1 in
+          let a2 = inj_term_of_texpr evd a2 in
+          TProp
+            (EConstr.mkApp
+               ( force mkrel
+               , [| rop.EBinRelT.source
+                  ; rop.EBinRelT.target
+                  ; t
+                  ; rop.EBinRelT.inj
+                  ; br
+                  ; a1
+                  ; a2 |] ))
+      with Not_found -> IProp e )
+    | PropUnOp {decl = rop} -> (
+      try
+        let t1 = trans_prop env evd a.(n - 1) in
+        match t1 with
+        | IProp _ -> IProp e
+        | _ ->
+          let t1 = inj_prop_of_tprop t1 in
+          TProp (EConstr.mkApp (force mkuprop_op, [|t; rop; t1|]))
+      with Not_found -> IProp e )
+    | _ -> IProp e
   with Not_found -> IProp e
 
 let unfold n env evd c =
@@ -984,14 +880,14 @@ let unfold n env evd c =
     match n with
     | None -> c
     | Some n ->
-        Tacred.unfoldn [(Locus.AllOccurrences, Names.EvalVarRef n)] env evd c
+      Tacred.unfoldn [(Locus.AllOccurrences, Names.EvalVarRef n)] env evd c
   in
   (* Reduce the term *)
-  let c = cbv (List.rev_append (force to_unfold)  unfold_decl) env evd c in
+  let c = cbv (List.rev_append (force to_unfold) unfold_decl) env evd c in
   c
 
 let trans_check_prop env evd t =
-  if is_prop  env evd t then
+  if is_prop env evd t then
     (*let t = Tacred.unfoldn [Locus.AllOccurrences, Names.EvalConstRef coq_not] env evd t in*)
     match trans_prop env evd t with IProp e -> None | TProp e -> Some e
   else None
@@ -1001,7 +897,7 @@ let trans_hyps env evd l =
     (fun acc (h, p) ->
       match trans_check_prop env evd p with
       | None -> acc
-      | Some p' -> (h, p, p') :: acc )
+      | Some p' -> (h, p, p') :: acc)
     [] (List.rev l)
 
 (* Only used if a direct rewrite fails *)
@@ -1016,7 +912,7 @@ let trans_hyp h t =
           let h' = fresh_id_in_env Id.Set.empty h env in
           tclTHENLIST
             [ letin_tac None (Names.Name n) t None
-                Locus.{onhyps= None; concl_occs= NoOccurrences}
+                Locus.{onhyps = None; concl_occs = NoOccurrences}
             ; assert_by (Name.Name h')
                 (EConstr.mkApp (force q, [|EConstr.mkVar n|]))
                 (tclTHEN
@@ -1027,19 +923,19 @@ let trans_hyp h t =
                 (h', Locus.InHyp)
             ; clear [n]
             ; (* [clear H] may fail if [h] has dependencies *)
-              tclTRY (clear [h]) ] )))
+              tclTRY (clear [h]) ])))
 
 let is_progress_rewrite evd t rew =
   match EConstr.kind evd rew with
   | App (c, [|lhs; rhs|]) ->
-      if EConstr.eq_constr evd (force iff) c then
-        (* This is a successful rewriting *)
-        not (EConstr.eq_constr evd lhs rhs)
-      else
-        CErrors.anomaly
-          Pp.(
-            str "is_progress_rewrite: not a rewrite"
-            ++ pr_constr (Global.env ()) evd rew)
+    if EConstr.eq_constr evd (force iff) c then
+      (* This is a successful rewriting *)
+      not (EConstr.eq_constr evd lhs rhs)
+    else
+      CErrors.anomaly
+        Pp.(
+          str "is_progress_rewrite: not a rewrite"
+          ++ pr_constr (Global.env ()) evd rew)
   | _ -> failwith "is_progress_rewrite: not even an application"
 
 let trans_hyp h t0 t =
@@ -1050,10 +946,10 @@ let trans_hyp h t0 t =
         let t' = unfold None env evd (EConstr.mkApp (force ieq, [|t|])) in
         if is_progress_rewrite evd t0 (get_type_of env evd t') then
           tclFIRST
-            [ Equality.general_rewrite_in true Locus.AllOccurrences true false
-                h t' false
+            [ Equality.general_rewrite_in true Locus.AllOccurrences true false h
+                t' false
             ; trans_hyp h t ]
-        else tclIDTAC ))
+        else tclIDTAC))
 
 let trans_concl t =
   Tacticals.New.(
@@ -1064,15 +960,15 @@ let trans_concl t =
         let t' = unfold None env evd (EConstr.mkApp (force ieq, [|t|])) in
         if is_progress_rewrite evd concl (get_type_of env evd t') then
           Equality.general_rewrite true Locus.AllOccurrences true false t'
-        else tclIDTAC ))
+        else tclIDTAC))
 
 let tclTHENOpt e tac tac' =
   match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac'
 
 let zify_tac =
   Proofview.Goal.enter (fun gl ->
-      Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"] ;
-      Coqlib.check_required_library ["Coq"; "micromega"; "ZifyInst"] ;
+      Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"];
+      Coqlib.check_required_library ["Coq"; "micromega"; "ZifyInst"];
       init_cache ();
       let evd = Tacmach.New.project gl in
       let env = Tacmach.New.pf_env gl in
@@ -1083,15 +979,16 @@ let zify_tac =
         (Tacticals.New.tclTHEN
            (Tacticals.New.tclTHENLIST
               (List.rev_map (fun (h, p, t) -> trans_hyp h p t) hyps))
-           (CstrTable.gen_cstr l)) )
+           (CstrTable.gen_cstr l)))
 
 let iter_specs tac =
   Tacticals.New.tclTHENLIST
-    (List.fold_left (fun acc d  -> tac d :: acc) [] (Spec.get ()))
+    (List.fold_left (fun acc d -> tac d :: acc) [] (Spec.get ()))
 
-
-let iter_specs (tac: Ltac_plugin.Tacinterp.Value.t) =
-    iter_specs (fun c -> Ltac_plugin.Tacinterp.Value.apply tac [Ltac_plugin.Tacinterp.Value.of_constr c])
+let iter_specs (tac : Ltac_plugin.Tacinterp.Value.t) =
+  iter_specs (fun c ->
+      Ltac_plugin.Tacinterp.Value.apply tac
+        [Ltac_plugin.Tacinterp.Value.of_constr c])
 
 let find_hyp evd t l =
   try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l))
@@ -1104,39 +1001,37 @@ let sat_constr c d =
       let hyps = Tacmach.New.pf_hyps_types gl in
       match EConstr.kind evd c with
       | App (c, args) ->
-          if Array.length args = 2 then (
-            let h1 =
-              Tacred.cbv_beta env evd
-                (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
+        if Array.length args = 2 then
+          let h1 =
+            Tacred.cbv_beta env evd
+              (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
+          in
+          let h2 =
+            Tacred.cbv_beta env evd
+              (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
+          in
+          match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with
+          | Some h1, Some h2 ->
+            let n =
+              Tactics.fresh_id_in_env Id.Set.empty
+                (Names.Id.of_string "__sat")
+                env
             in
-            let h2 =
-              Tacred.cbv_beta env evd
-                (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
+            let trm =
+              EConstr.mkApp
+                ( d.ESatT.satOK
+                , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] )
             in
-            match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with
-            | Some h1, Some h2 ->
-                let n =
-                  Tactics.fresh_id_in_env Id.Set.empty
-                    (Names.Id.of_string "__sat")
-                    env
-                in
-                let trm =
-                  EConstr.mkApp
-                    ( d.ESatT.satOK
-                    , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|]
-                    )
-                in
-                Tactics.pose_proof (Names.Name n) trm
-            | _, _ -> Tacticals.New.tclIDTAC )
-          else Tacticals.New.tclIDTAC
-      | _ -> Tacticals.New.tclIDTAC )
-
+            Tactics.pose_proof (Names.Name n) trm
+          | _, _ -> Tacticals.New.tclIDTAC
+        else Tacticals.New.tclIDTAC
+      | _ -> Tacticals.New.tclIDTAC)
 
 let get_all_sat env evd c =
-  List.fold_left (fun acc e ->
-      match e with
-      | (_,Saturate s) -> s::acc
-      |  _   -> acc) [] (HConstr.find_all c !saturate_cache )
+  List.fold_left
+    (fun acc e -> match e with _, Saturate s -> s :: acc | _ -> acc)
+    []
+    (HConstr.find_all c !saturate_cache)
 
 let saturate =
   Proofview.Goal.enter (fun gl ->
@@ -1149,21 +1044,19 @@ let saturate =
       let rec sat t =
         match EConstr.kind evd t with
         | App (c, args) ->
-            sat c ;
-            Array.iter sat args ;
-            if Array.length args = 2 then
-              let ds = get_all_sat env evd c in
-              if ds = [] then ()
-              else (
-                List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds )
-            else ()
+          sat c;
+          Array.iter sat args;
+          if Array.length args = 2 then
+            let ds = get_all_sat env evd c in
+            if ds = [] then ()
+            else List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds
+          else ()
         | Prod (a, t1, t2) when a.Context.binder_name = Names.Anonymous ->
-            sat t1 ; sat t2
+          sat t1; sat t2
         | _ -> ()
       in
       (* Collect all the potential saturation lemma *)
-      sat concl ;
-      List.iter (fun (_, t) -> sat t) hyps ;
+      sat concl;
+      List.iter (fun (_, t) -> sat t) hyps;
       Tacticals.New.tclTHENLIST
-        (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table [])
-  )
+        (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table []))