diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-11 09:34:12 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-11 09:34:12 +0000 |
| commit | 47b37874d6b0ec1b8a5f69655d4cab417ed4a05b (patch) | |
| tree | e14c076aa1bfd9ca42e40d34ff2b55775103b181 | |
| parent | d8cd2855d4e3e2f77dec93b6f1dffd74a5af8468 (diff) | |
bug cast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1745 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 66b431f17..801a411ab 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 218bb7141..3d6d35a4e 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 *) |