1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
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 =
|
