Use ocp-indent and reindent

Author: kit-ty-kate

.ocp-indent

@@ -0,0 +1,2 @@
+JaneStreet
+match_clause = 4

src/mtac2Interp.ml

@@ -11,13 +11,13 @@ let get_its_info gls = Mtac2ProofInfos.get_info gls.Evd.sigma gls.it
 (**  *)
 let tcl_change_info_gen info_gen =
   (fun gls ->
-    let it = Evd.sig_it gls in
-    let concl = Tacmach.pf_concl gls in
-    let hyps = Goal.V82.hyps (Tacmach.project gls) it in
-    let extra = Goal.V82.extra (Tacmach.project gls) it in
-    let (gl,ev,sigma) = Goal.V82.mk_goal (Tacmach.project gls) hyps concl (info_gen extra) in
-    let sigma = Goal.V82.partial_solution sigma it ev in
-    {it = [gl] ; sigma= sigma; } )
+     let it = Evd.sig_it gls in
+     let concl = Tacmach.pf_concl gls in
+     let hyps = Goal.V82.hyps (Tacmach.project gls) it in
+     let extra = Goal.V82.extra (Tacmach.project gls) it in
+     let (gl,ev,sigma) = Goal.V82.mk_goal (Tacmach.project gls) hyps concl (info_gen extra) in
+     let sigma = Goal.V82.partial_solution sigma it ev in
+     {it = [gl] ; sigma= sigma; } )
 
 (** Updates the info of the evar maps *)
 let tcl_change_info info gls =
@@ -56,7 +56,7 @@ let interp_mproof_command () =
 (** Interpreter of a mtactic *)
 let interp_instr instr =
   match instr with
-    | Mtac2Instr.Mtac2_constr c -> Mtac2Run.run_tac c
+  | Mtac2Instr.Mtac2_constr c -> Mtac2Run.run_tac c
 
 (** Interpreter of a constr :
     - Interpretes the constr

src/mtac2ProofInfos.ml

@@ -1,12 +1,11 @@
 (**
-    This module concerns the state of the proof tree
+   This module concerns the state of the proof tree
 *)
 
 (**  *)
 type split_tree=
     Skip_patt of Names.Id.Set.t * split_tree
-  | Split_patt of Names.Id.Set.t * Names.inductive *
-		(bool array * (Names.Id.Set.t * split_tree) option) array
+  | Split_patt of Names.Id.Set.t * Names.inductive * (bool array * (Names.Id.Set.t * split_tree) option) array
   | Close_patt of split_tree
   | End_patt of (Names.Id.t * (int * int))
 
@@ -19,14 +18,14 @@ type elim_kind =
 type recpath = int option*Declarations.wf_paths
 
 type per_info =
-    {per_casee:Term.constr;
-     per_ctype:Term.types;
-     per_ind:Names.inductive;
-     per_pred:Term.constr;
-     per_args:Term.constr list;
-     per_params:Term.constr list;
-     per_nparams:int;
-     per_wf:recpath}
+  {per_casee:Term.constr;
+   per_ctype:Term.types;
+   per_ind:Names.inductive;
+   per_pred:Term.constr;
+   per_args:Term.constr list;
+   per_params:Term.constr list;
+   per_nparams:int;
+   per_wf:recpath}
 
 type elim_type =
     ET_Case_analysis
@@ -39,7 +38,7 @@ type stack_info =
   | Focus_claim
 
 type pm_info =
-    { pm_stack : stack_info list}
+  { pm_stack : stack_info list}
 
 (** Create a new field in datatype used to store additional information in evar maps*)
 let info = Evd.Store.field ()
@@ -61,7 +60,7 @@ let proof_cond = Proof.no_cond proof_focus
 (** focus on the proof *)
 let focus p =
   let inf = get_stack p in
-Printf.printf "____focus\n%!";
+  Printf.printf "____focus\n%!";
   Proof_global.simple_with_current_proof
     (fun _ -> Proof.focus proof_cond inf 1)
 

src/mtac2Run.ml

@@ -28,9 +28,9 @@ let run_tac t =
     let (sigma, t) = pretypeT env sigma concl c in
     let r = run (env, sigma) c in
     match r with
-      | Val (sigma', _, v) ->
-	(Proofview.Unsafe.tclEVARS sigma')
-	<*> (Proofview.Refine.refine ~unsafe:false (fun s->(s, v)))
-      | Err (_, _, e) ->
-	Errors.error ("Uncaught exception: " ^ (Pp.string_of_ppcmds (Termops.print_constr e)))
+    | Val (sigma', _, v) ->
+        (Proofview.Unsafe.tclEVARS sigma')
+        <*> (Proofview.Refine.refine ~unsafe:false (fun s->(s, v)))
+    | Err (_, _, e) ->
+        Errors.error ("Uncaught exception: " ^ (Pp.string_of_ppcmds (Termops.print_constr e)))
   end