diff options
| author | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
| commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
| tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /plugins/funind/indfun_common.ml | |
| parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
| parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) | |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 76fcd5ec87..e9102e9c82 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -1,8 +1,10 @@ open Names open Pp +open Constr open Libnames open Globnames open Refiner + let mk_prefix pre id = Id.of_string (pre^(Id.to_string id)) let mk_rel_id = mk_prefix "R_" let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct" @@ -111,7 +113,7 @@ let const_of_id id = (str "cannot find " ++ Id.print id) let def_of_const t = - match (Term.kind_of_term t) with + match Constr.kind t with Term.Const sp -> (try (match Environ.constant_opt_value_in (Global.env()) sp with | Some c -> c @@ -330,8 +332,6 @@ let discharge_Function (_,finfos) = is_general = finfos.is_general } -open Term - let pr_ocst c = Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) @@ -545,9 +545,9 @@ let prodn n env b = (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *) let compose_prod l b = prodn (List.length l) l b -type tcc_lemma_value = +type tcc_lemma_value = | Undefined - | Value of Term.constr + | Value of constr | Not_needed (* We only "purify" on exceptions *) |