Fix typos

2 files changed, 142 insertions, 0 deletions

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@braud-santoni.eu>
+Reviewed-by: Nicolas Braud-Santoni <nicolas@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