aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-05-04 10:36:43 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-05-04 10:36:53 +0200
commitdd7cf3a8086fa8a08a421314caec8543ba62226b (patch)
treed5657a668e9c5ee456813ebc4f90f5e402e9f883 /plugins/extraction
parent1dd8d826592507046b35128800578149021dab4c (diff)
Handle primitive projections inside types when extracting (bug #4616).
Note that extracting terms containing primitive projections is still utterly broken, so don't use them.
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extraction.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 10644da25..667721e67 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -285,7 +285,7 @@ let rec extract_type env db j c args =
| Ind ((kn,i),u) ->
let s = (extract_ind env kn).ind_packets.(i).ip_sign in
extract_type_app env db (IndRef (kn,i),s) args
- | Case _ | Fix _ | CoFix _ -> Tunknown
+ | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown
| _ -> assert false
(*s Auxiliary function dealing with type application.