aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
authorMaxime Dénès2017-10-20 11:01:36 +0200
committerMaxime Dénès2017-10-20 11:01:36 +0200
commit09525d09e414d3582595ffd141702e69a9a2efb9 (patch)
tree29b9077bb40339029dd18de7208545e9b336cecb /plugins/extraction
parent6bda57bd75efe55fe1f7774f932e9ef5a65aeaaf (diff)
parentd8177f283eec2b00d9dd7ea38e57e150e9b00188 (diff)
Merge PR #960: Uniformize references to Bugzilla
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 cf97ae3ab8..4bc3dba36e 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 0f537abece..f708307c38 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') ->