diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-13 17:47:24 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-13 19:11:10 +0200 |
commit | 3a7095f9f6a09a4461c2124b0020dfe37962de26 (patch) | |
tree | 02485f6b975a1c9b59f80fb8409ac5a614962a04 /tactics/inv.ml | |
parent | 90d52ae25f08c5d1d58685e31073b8f3f37aad49 (diff) |
Safer typing primitives.
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
Diffstat (limited to 'tactics/inv.ml')
-rw-r--r-- | tactics/inv.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 5502356fb..ef115aea0 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -123,13 +123,13 @@ let make_inv_predicate env evd indf realargs id status concl = let refl_term = eqdata.Coqlib.refl in let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in - let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in let args = refl :: args in build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in - let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args @@ -437,7 +437,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = - try pf_apply Tacred.reduce_to_atomic_ind gl (pf_type_of gl c) + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) with UserError _ -> let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in Errors.errorlabstrm "" msg |