From 4bd88e8337ba04e0575150d9df1400fc96fa56af Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Sat, 23 Jul 2016 16:32:24 -0400 Subject: Fix typos --- debian/patches/0001-Fix-typos.patch | 141 ++++++++++++++++++++++++++++++++++++ debian/patches/series | 1 + 2 files changed, 142 insertions(+) create mode 100644 debian/patches/0001-Fix-typos.patch create mode 100644 debian/patches/series diff --git a/debian/patches/0001-Fix-typos.patch b/debian/patches/0001-Fix-typos.patch new file mode 100644 index 0000000..44ba6ac --- /dev/null +++ b/debian/patches/0001-Fix-typos.patch @@ -0,0 +1,141 @@ +Subject: Fix typos +From: Nicolas Braud-Santoni +Reviewed-by: Nicolas Braud-Santoni +Last-Update: 2016-07-23 +Forwarded: https://github.com/coq-contribs/aac-tactics/pull/2 +Applied-Upstream: no + +--- + Caveats.v | 4 ++-- + coq.ml | 2 +- + matcher.ml | 4 ++-- + print.ml | 2 +- + rewrite.ml4 | 2 +- + theory.ml | 10 +++++----- + 6 files changed, 12 insertions(+), 12 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..0677b99 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 +@@ -724,7 +724,7 @@ module Trans = struct + (* [t_of_constr] buils a the abstract syntax tree of a constr, + updating in place the environment. Doing so, we infer all the + morphisms and the AC/A operators. It is mandatory to do so both +- for the pattern and the term, since AC symbols can occur in one ++ for the pattern and the term, since AC symbols can occurr in one + and not the other *) + let t_of_constr goal rlt envs (l,r) = + let goal = Gather.gather goal rlt envs l in diff --git a/debian/patches/series b/debian/patches/series new file mode 100644 index 0000000..31091a9 --- /dev/null +++ b/debian/patches/series @@ -0,0 +1 @@ +0001-Fix-typos.patch -- cgit v1.2.3