aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-10-19 16:25:40 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-10-19 16:25:40 +0200
commit56b562e057bbce736786cf1df16ba6e40dde8f30 (patch)
tree79385990b1998ec93e2f23b12a7c15ddff3f473d /plugins/extraction
parentfb1478d2cd59991e8d2fc2e07dacad505ef110b7 (diff)
Moving bug numbers to BZ# format in the source code.
Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/CHANGES4
-rw-r--r--plugins/extraction/haskell.ml2
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index cf97ae3ab..4bc3dba36 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -54,7 +54,7 @@ but also a few steps toward a more user-friendly extraction:
* bug fixes:
- many concerning Records.
-- a Stack Overflow with mutual inductive (PR#320)
+- a Stack Overflow with mutual inductive (BZ#320)
- some optimizations have been removed since they were not type-safe:
For example if e has type: type 'x a = A
Then: match e with A -> A -----X----> e
@@ -125,7 +125,7 @@ but also a few steps toward a more user-friendly extraction:
- the dummy constant "__" have changed. see README
- - a few bug-fixes (#191 and others)
+ - a few bug-fixes (BZ#191 and others)
7.2 -> 7.3
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 0f537abec..f708307c3 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -145,7 +145,7 @@ let rec pp_expr par env args =
| MLrel n ->
let id = get_db_name n env in
(* Try to survive to the occurrence of a Dummy rel.
- TODO: we should get rid of this hack (cf. #592) *)
+ TODO: we should get rid of this hack (cf. BZ#592) *)
let id = if Id.equal id dummy_name then Id.of_string "__" else id in
apply (Id.print id)
| MLapp (f,args') ->