[Pkg-ocaml-maint-commits] [aac-tactics] 03/06: aac for Coq 8.6
Enrico Tassi
gareuselesinge at moszumanska.debian.org
Wed Dec 28 13:47:56 UTC 2016
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 <gareuselesinge at 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 <gareuselesinge at 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 <nicolas at braud-santoni.eu>
-Reviewed-by: Matej Košík <matej.kosik at 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
More information about the Pkg-ocaml-maint-commits
mailing list