From 3a7095f9f6a09a4461c2124b0020dfe37962de26 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2015 17:47:24 +0200
Subject: 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.
---
 plugins/omega/coq_omega.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/omega')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4e2696dfdb..710a2394d3 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1689,7 +1689,7 @@ let onClearedName2 id tac =
 
 let destructure_hyps =
   Proofview.Goal.nf_enter begin fun gl ->
-  let type_of = Tacmach.New.pf_type_of gl in
+  let type_of = Tacmach.New.pf_unsafe_type_of gl in
   let decidability = Tacmach.New.of_old decidability gl in
   let pf_nf = Tacmach.New.of_old pf_nf gl in
     let rec loop = function
-- 
cgit v1.2.3