diff options
| -rw-r--r-- | plugins/funind/glob_termops.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 30 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 7 |
3 files changed, 25 insertions, 14 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index b4ca1073c..41eb48657 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -562,7 +562,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect (* we first (pseudo) understand [rt] and get back the computed evar_map *) (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) - let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in + let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in let ctx, f = Evarutil.nf_evars_and_universes ctx in (* then we map [rt] to replace the implicit holes by their values *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8809558ff..6700748eb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -378,10 +378,10 @@ let check_evars_are_solved env current_sigma init_sigma = let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in check_evars_are_solved env current_sigma frozen -let process_inference_flags flags env initial_sigma (sigma,c) = +let process_inference_flags flags env initial_sigma (sigma,c,cty) = let sigma = solve_remaining_evars flags env sigma initial_sigma in let c = if flags.expand_evars then nf_evar sigma c else c in - sigma,c + sigma,c,cty let adjust_evar_source evdref na c = match na, kind !evdref c with @@ -1173,15 +1173,18 @@ let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env sigma in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in - let c' = match kind with + let c', c'_ty = match kind with | WithoutTypeConstraint -> - (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val + let j = pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c in + j.uj_val, j.uj_type | OfType exptyp -> - (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val + let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c in + j.uj_val, j.uj_type | IsType -> - (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val + let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c in + tj.utj_val, mkSort tj.utj_type in - process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c',c'_ty) let default_inference_flags fail = { use_typeclasses = true; @@ -1201,7 +1204,7 @@ let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false let ise_pretype_gen_ctx flags env sigma lvar kind c = - let evd, c = ise_pretype_gen flags env sigma lvar kind c in + let evd, c, _ = ise_pretype_gen flags env sigma lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd @@ -1213,12 +1216,15 @@ let understand env sigma c = ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c -let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = - let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in - (sigma, c) +let understand_tcc_ty ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = + ise_pretype_gen flags env sigma empty_lvar expected_type c + +let understand_tcc ?flags env sigma ?expected_type c = + let sigma, c, _ = understand_tcc_ty ?flags env sigma ?expected_type c in + sigma, c let understand_ltac flags env sigma lvar kind c = - let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in + let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) let pretype k0 resolve_tc typcon env evdref lvar t = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index fe10be9e7..864768fe5 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -58,6 +58,11 @@ val all_and_fail_flags : inference_flags val understand_tcc : ?flags:inference_flags -> env -> evar_map -> ?expected_type:typing_constraint -> glob_constr -> evar_map * constr +(** As [understand_tcc] but also returns the type of the elaborated term. + The [expand_evars] flag is not applied to the type (only to the term). *) +val understand_tcc_ty : ?flags:inference_flags -> env -> evar_map -> + ?expected_type:typing_constraint -> glob_constr -> evar_map * constr * types + (** More general entry point with evars from ltac *) (** Generic call to the interpreter from glob_constr to constr @@ -116,7 +121,7 @@ val pretype_type : val ise_pretype_gen : inference_flags -> env -> evar_map -> - ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr + ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types (**/**) |