From a8c0742d53ca8802a3032d801e4a5e169851078e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:07:18 +0000 Subject: 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(-) delete mode 100644 debian/patches/0001-Fix-typos.patch delete mode 100644 debian/patches/series 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 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 -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 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 -- cgit v1.2.3