This is an automated email from the git hooks/post-receive script.

gareuselesinge pushed a commit to branch master
in repository aac-tactics.

commit a8c0742d53ca8802a3032d801e4a5e169851078e
Author: Enrico Tassi <gareuselesi...@debian.org>
Date:   Tue Dec 27 16:07:18 2016 +0000

    aac for Coq 8.6
---
 debian/changelog                         |   8 ++
 debian/libaac-tactics-ocaml-dev.ocamldoc |   2 +-
 debian/patches/0001-Fix-typos.patch      | 132 -------------------------------
 debian/patches/series                    |   1 -
 4 files changed, 9 insertions(+), 134 deletions(-)

diff --git a/debian/changelog b/debian/changelog
index dbe40b7..abdad05 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,11 @@
+aac-tactics (8.6-1) unstable; urgency=medium
+
+  * Team upload
+  * New upstream release
+  * Remove patch 001-fix-typos, applied upstream
+
+ -- Enrico Tassi <gareuselesi...@debian.org>  Tue, 27 Dec 2016 16:06:51 +0000
+
 aac-tactics (8.5.1-1) unstable; urgency=medium
 
   * Team upload
diff --git a/debian/libaac-tactics-ocaml-dev.ocamldoc 
b/debian/libaac-tactics-ocaml-dev.ocamldoc
index 83a7cff..f59e96e 100644
--- a/debian/libaac-tactics-ocaml-dev.ocamldoc
+++ b/debian/libaac-tactics-ocaml-dev.ocamldoc
@@ -1,3 +1,3 @@
 -rectypes
--I /usr/lib/coq/kernel -I /usr/lib/coq/proofs -I /usr/lib/coq/pretyping
+-I /usr/lib/coq/kernel -I /usr/lib/coq/proofs -I /usr/lib/coq/pretyping -I 
/usr/lib/coq/engine
 --include debian/libaac-tactics-ocaml-dev/usr/lib/coq
diff --git a/debian/patches/0001-Fix-typos.patch 
b/debian/patches/0001-Fix-typos.patch
deleted file mode 100644
index 852914f..0000000
--- a/debian/patches/0001-Fix-typos.patch
+++ /dev/null
@@ -1,132 +0,0 @@
-Subject: Fix typos
-From: Nicolas Braud-Santoni <nico...@braud-santoni.eu>
-Reviewed-by: Matej Košík <matej.ko...@inria.fr>
-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
diff --git a/debian/patches/series b/debian/patches/series
deleted file mode 100644
index 31091a9..0000000
--- a/debian/patches/series
+++ /dev/null
@@ -1 +0,0 @@
-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

_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits

Reply via email to