Correct spelling errors

2 files changed, 60 insertions, 0 deletions

diff --git a/debian/patches/series b/debian/patches/series
index 3a1b8d0f..4f1f3fcf 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -7,3 +7,4 @@ avoid-usr-bin-env.patch
 python-scripts-libraries.patch
 skip-dot-pc.patch
 remove-ssrmatching.patch
+spelling.patch
diff --git a/debian/patches/spelling.patch b/debian/patches/spelling.patch
new file mode 100644
index 00000000..81e27170
--- /dev/null
+++ b/debian/patches/spelling.patch
@@ -0,0 +1,59 @@
+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 =