diff options
| author | Pierre-Marie Pédrot | 2015-10-29 18:18:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-29 19:03:38 +0100 |
| commit | f02f64a21863ce03f2da4ff04cd003051f96801f (patch) | |
| tree | 601fded539120c931b4ece1cff9d0790bdd82fea /plugins | |
| parent | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (diff) | |
Removing some goal unsafeness in inductive schemes.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c47602bda0..bbe2f1a3ad 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -12,6 +12,7 @@ open Tactics open Indfun_common open Functional_principles_proofs open Misctypes +open Sigma.Notations exception Toberemoved_with_rel of int*constr exception Toberemoved @@ -648,12 +649,15 @@ let build_case_scheme fa = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes in - let ind_fun = + let (ind, sf) = let ind = first_fun_kn,funs_indexes in (ind,Univ.Instance.empty)(*FIXME*),prop_sort in - let sigma, scheme = - (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (scheme, sigma, _) = + Indrec.build_case_analysis_scheme_default env sigma ind sf + in + let sigma = Sigma.to_evar_map sigma in let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in let sorts = (fun (_,_,x) -> |