diff options
Diffstat (limited to 'contrib/extraction/extraction.ml')
| -rw-r--r-- | contrib/extraction/extraction.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index e6acb73ab..2c6fb88f6 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -144,14 +144,6 @@ let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c) let is_axiom sp = (Global.lookup_constant sp).const_body = None -(* TODO: Could we export the one inside reductionops *) - -let rec find_conclusion env c = - let t = whd_betadeltaiota env none c in - match kind_of_term t with - | Prod (x,t,c0) -> find_conclusion (push_rel (x,None,t) env) c0 - | t -> t - (*s [flag_of_type] transforms a type [t] into a [flag]. Really important function. *) |