From: Benjamin Barenblat <bbaren@debian.org>
Subject: Correct spelling errors
Forwarded: no
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -409,7 +409,7 @@
       match exp, exp2 with
       | Some expa, Some expb -> constr_expr ogname expa expb
       | None, None -> ()
-      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (1)")
+      | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (1)")
     in
     let local_binder_expr ogname exp exp2 =
       match exp, exp2 with
@@ -421,7 +421,7 @@
       | CLocalPattern p, CLocalPattern p2 ->
         let (p,ty), (p2,ty2) = p.v,p2.v in
         constr_expr_opt ogname ty ty2
-      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (2)")
+      | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
     in
     let recursion_order_expr ogname exp exp2 =
       match exp, exp2 with
@@ -431,7 +431,7 @@
       | CMeasureRec (m,r), CMeasureRec (m2,r2) ->
         constr_expr ogname m m2;
         constr_expr_opt ogname r r2
-      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (3)")
+      | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)")
     in
     let fix_expr ogname exp exp2 =
       let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in
@@ -515,7 +515,7 @@
       | CastNative a, CastNative a2 ->
         constr_expr ogname a a2
       | CastCoerce, CastCoerce -> ()
-      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (4)"))
+      | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)"))
     | CNotation (ntn,args), CNotation (ntn2,args2) ->
       constr_notation_substitution ogname args args2
     | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) ->
@@ -523,7 +523,7 @@
     | CPrim p, CPrim p2 -> ()
     | CDelimiters (key,e), CDelimiters (key2,e2) ->
       constr_expr ogname e e2
-    | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (5)")
+    | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (5)")
     end
   in
 
@@ -626,7 +626,7 @@
         in
         Goal.Set.iter (fun ng -> ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og) add_gs;
         !ng_to_og
-      with Not_found -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (6)")
+      with Not_found -> raise (Diff_Failure "Unable to match goals between old and new proof states (6)")
     end
 
 let make_goal_map op np =