diff options
| -rw-r--r-- | contrib/extraction/extraction.ml | 2 | ||||
| -rw-r--r-- | contrib/extraction/test_extraction.v | 4 |
2 files changed, 5 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 66b431f173..801a411ab7 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -99,7 +99,7 @@ type extraction_result = let none = Evd.empty -let type_of env c = Typing.type_of env Evd.empty c +let type_of env c = Typing.type_of env Evd.empty (strip_outer_cast c) let whd_betaiotalet = clos_norm_flags (UNIFORM, red_add betaiota_red ZETA) diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v index 218bb71413..3d6d35a4e9 100644 --- a/contrib/extraction/test_extraction.v +++ b/contrib/extraction/test_extraction.v @@ -139,6 +139,10 @@ Inductive tp1bis : Set := Tbis : tp2bis -> tp1bis with tp2bis : Set := T'bis : (C:Set)(c:C)tp1bis->tp2bis. +(* casts *) + +Extraction (True :: Type). + (* example needing Obj.magic *) (* hybrids *) |