diff options
| author |  Nicolas Braud-Santoni <nicolas@braud-santoni.eu> | 2016-07-25 16:53:39 -0400 |
|---|---|---|
| committer | Nicolas Braud-Santoni <nicolas@braud-santoni.eu> | 2016-07-25 16:53:39 -0400 |
| commit | eec22d00522c7f0438b30f412c5e6bef03842f24 (patch) | |
| tree | 47dcf40ff517b80fa812e31119dd14ae925b1bd3 | |
| parent | d4116c6dca453eff2be852593e4a6a32ff1e5fbc (diff) | |
Update 0001-Fix-typos.patch
The change was merged upstream (and an error was fixed)
| -rw-r--r-- | debian/patches/0001-Fix-typos.patch | 31 |
1 files changed, 11 insertions, 20 deletions
diff --git a/debian/patches/0001-Fix-typos.patch b/debian/patches/0001-Fix-typos.patch index 44ba6ac..852914f 100644 --- a/debian/patches/0001-Fix-typos.patch +++ b/debian/patches/0001-Fix-typos.patch @@ -1,18 +1,18 @@ 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 +Reviewed-by: Matej Košík <matej.kosik@inria.fr> +Last-Update: 2016-07-25 Forwarded: https://github.com/coq-contribs/aac-tactics/pull/2 -Applied-Upstream: no +Applied-Upstream: yes --- - 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(-) + 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 @@ -99,7 +99,7 @@ index b3e52e0..742a225 100644 ) ) goal diff --git a/theory.ml b/theory.ml -index a5229fa..0677b99 100644 +index a5229fa..e1098c6 100644 --- a/theory.ml +++ b/theory.ml @@ -424,15 +424,15 @@ module Trans = struct @@ -130,12 +130,3 @@ index a5229fa..0677b99 100644 (** [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 |