Subject: Fix typos From: Nicolas Braud-Santoni Reviewed-by: Matej Košík 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