[Pkg-ocaml-maint-commits] [aac-tactics] 04/04: Fix typos
Nicolas Braud-Santoni
nicolas at braud-santoni.eu
Sun Jul 24 02:22:36 UTC 2016
This is an automated email from the git hooks/post-receive script.
nicoo-guest pushed a commit to branch patch-queue/master
in repository aac-tactics.
commit 3069277d6b95ddbba22d7ac0441a05e8dcc0ba7d
Author: Nicolas Braud-Santoni <nicolas at braud-santoni.eu>
Date: Sat Jul 23 16:32:02 2016 -0400
Fix typos
---
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
--
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