[Pkg-ocaml-maint-commits] [aac-tactics] 07/09: Fix typos
Nicolas Braud-Santoni
nicolas at braud-santoni.eu
Sun Jul 24 02:17:58 UTC 2016
This is an automated email from the git hooks/post-receive script.
nicoo-guest pushed a commit to branch master
in repository aac-tactics.
commit 4bd88e8337ba04e0575150d9df1400fc96fa56af
Author: Nicolas Braud-Santoni <nicolas at braud-santoni.eu>
Date: Sat Jul 23 16:32:24 2016 -0400
Fix typos
---
debian/patches/0001-Fix-typos.patch | 141 ++++++++++++++++++++++++++++++++++++
debian/patches/series | 1 +
2 files changed, 142 insertions(+)
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 <nicolas at braud-santoni.eu>
+Reviewed-by: Nicolas Braud-Santoni <nicolas at braud-santoni.eu>
+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
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git
More information about the Pkg-ocaml-maint-commits
mailing list