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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
Subject: Fix typos
From: Nicolas Braud-Santoni <nicolas@braud-santoni.eu>
Reviewed-by: Matej Košík <matej.kosik@inria.fr>
Last-Update: 2016-07-25
Forwarded: https://github.com/coq-contribs/aac-tactics/pull/2
Applied-Upstream: yes
---
Caveats.v | 4 ++--
coq.ml | 2 +-
matcher.ml | 4 ++--
print.ml | 2 +-
rewrite.ml4 | 2 +-
theory.ml | 8 ++++----
6 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/Caveats.v b/Caveats.v
index a7967cc..9ec0204 100644
--- a/Caveats.v
+++ b/Caveats.v
@@ -333,7 +333,7 @@ Goal a+b*c = c.
*)
Abort.
-(** **** If the pattern is a unit or can be instanciated to be equal
+(** **** If the pattern is a unit or can be instantiated to be equal
to a unit:
The heuristic is to make the unit appear at each possible position
@@ -350,7 +350,7 @@ Goal a+b+c = c.
(** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*)
Abort.
-(** *** Another example of the former case is the following, where the hypothesis can be instanciated to be equal to [1] *)
+(** *** Another example of the former case is the following, where the hypothesis can be instantiated to be equal to [1] *)
Hypothesis H : forall x y, (x+y)*x = x*x + y *x.
Goal a*a+b*a + c = c.
(** Here, only one solution if we use the aac_instance tactic *)
diff --git a/coq.ml b/coq.ml
index 97154e2..fcb5691 100755
--- a/coq.ml
+++ b/coq.ml
@@ -474,7 +474,7 @@ let recompose_prod
em, acc
(* no fresh evars : instead, use a lambda abstraction around an
- application to handle non-instanciated variables. *)
+ application to handle non-instantiated variables. *)
let recompose_prod'
(context : Context.rel_context)
diff --git a/matcher.ml b/matcher.ml
index 2fd0517..4e93e88 100644
--- a/matcher.ml
+++ b/matcher.ml
@@ -1094,7 +1094,7 @@ let unit_warning p ~nullif ~unitif =
begin
Pp.msg_warning
(Pp.str
- "[aac_tactics] This pattern can be instanciated to match units, some solutions can be missing");
+ "[aac_tactics] This pattern can be instantiated to match units, some solutions can be missing");
end
;;
@@ -1127,7 +1127,7 @@ let unit_warning p ~nullif ~unitif =
pattern uninstantiated. We do so in order to allow interaction
with the user, to choose the env.
- Strange patterms like x*y*x can be instanciated by nothing, inside
+ Strange patterms like x*y*x can be instantiated by nothing, inside
a product. Therefore, we need to check that all the term is not
going into the context. With proper support for interaction with
the user, we should lift these tests. However, at the moment, they
diff --git a/print.ml b/print.ml
index 0305158..a3018cf 100644
--- a/print.ml
+++ b/print.ml
@@ -51,7 +51,7 @@ remain compatible with the parameters of {!aac_rewrite} *)
let pp_all pt : (int * Terms.t * named_env Search_monad.m) Search_monad.m -> Pp.std_ppcmds = fun m ->
let _,s = Search_monad.fold
(fun (size,context,envm) (n,acc) ->
- let s = str (Printf.sprintf "occurence %i: transitivity through " n) in
+ let s = str (Printf.sprintf "occurrence %i: transitivity through " n) in
let s = s ++ pt context ++ str "\n" in
let s = if trivial_substitution envm then s else
s ++ str (Printf.sprintf "%i possible(s) substitution(s)" (Search_monad.count envm) )
diff --git a/rewrite.ml4 b/rewrite.ml4
index b3e52e0..742a225 100644
--- a/rewrite.ml4
+++ b/rewrite.ml4
@@ -435,7 +435,7 @@ let aac_rewrite ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
| NoSolutions ->
Tacticals.tclFAIL 0
(Pp.str (if occ_subterm = None && occ_sol = None
- then "No matching occurence modulo AC found"
+ then "No matching occurrence modulo AC found"
else "No such solution"))
)
) goal
diff --git a/theory.ml b/theory.ml
index a5229fa..e1098c6 100644
--- a/theory.ml
+++ b/theory.ml
@@ -424,15 +424,15 @@ module Trans = struct
with Not_found -> assert false
(********************************************)
- (* (\* Gather the occuring AC/A symbols *\) *)
+ (* (\* Gather the occurring AC/A symbols *\) *)
(********************************************)
(** This modules exhibit a function that memoize in the environment
- all the AC/A operators as well as the morphism that occur. This
+ all the AC/A operators as well as the morphism that occurr. This
staging process allows us to prefer AC/A operators over raw
morphisms. Moreover, for each AC/A operators, we need to try to
infer units. Otherwise, we do not have [x * y * x <= a * a] since 1
- does not occur.
+ does not occurr.
But, do we also need to check whether constants are
units. Otherwise, we do not have the ability to rewrite [0 = a +
@@ -679,7 +679,7 @@ module Trans = struct
(* TODO: is it the only source of invalid use that fall
into this catch_all ? *)
| e ->
- user_error "Cannot handle this kind of hypotheses (variables occuring under a function symbol which is not a proper morphism)."
+ user_error "Cannot handle this kind of hypotheses (variables occurring under a function symbol which is not a proper morphism)."
(** [t_of_constr goal rlt envs cstr] builds the abstract syntax tree
of the term [cstr]. Doing so, it modifies the environment of
|
