diff options
| author | Gaëtan Gilbert | 2017-10-27 14:03:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 75508769762372043387c67a9abe94e8f940e80a (patch) | |
| tree | 3f63e7790e9f3b6e7384b0a445d62cfa7edbe829 /plugins/extraction | |
| parent | a0e16c9e5c3f88a8b72935dd4877f13388640f69 (diff) | |
Add a non-cumulative impredicative universe SProp.
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index ef6c07bff2..877ea9a537 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -73,13 +73,18 @@ type flag = info * scheme (*s [flag_of_type] transforms a type [t] into a [flag]. Really important function. *) +let info_of_family = function + | InSProp | InProp -> Logic + | InSet | InType -> Info + +let info_of_sort s = info_of_family (Sorts.family s) + let rec flag_of_type env sg t : flag = let t = whd_all env sg t in match EConstr.kind sg t with | Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c - | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme) - | Sort _ -> (Info,TypeScheme) - | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default) + | Sort s -> (info_of_sort (EConstr.ESorts.kind sg s),TypeScheme) + | _ -> (info_of_family (sort_of env sg t),Default) (*s Two particular cases of [flag_of_type]. *) |