diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
| commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
| tree | 1a46f0142a85df553388c932110793881f3af52f /plugins/funind/functional_principles_types.ml | |
| parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) | |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 6df9d574..00e966fb 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -142,12 +142,6 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *) res in - let rec has_dummy_var t = - fold_constr - (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t)) - false - t - in let rec compute_new_princ_type remove env pre_princ : types*(constr list) = let (new_princ_type,_) as res = match kind_of_term pre_princ with |