From 836b9faa8797a2802c189e782469f8d2e467d894 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 16:15:05 +0200
Subject: Univs: fix evar_map leaks bugs in Function

The evar_map's that are used to typecheck terms must now always be
initialized with the global universe graphs using Evd.from_env, so any
failure to initialize and thread evar_map's correctly results in errors.
---
 plugins/funind/invfun.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 89ceb751a4..d979401424 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -760,7 +760,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
   let funs_constr = Array.map mkConstU funs  in
   States.with_state_protection_on_exception
     (fun () ->
-     let evd = ref Evd.empty in 
+     let env = Global.env () in
+     let evd = ref (Evd.from_env env) in 
      let graphs_constr = Array.map mkInd graphs in
      let lemmas_types_infos =
        Util.Array.map2_i
@@ -829,7 +830,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 
       )
       funs;
-    (* let evd = ref Evd.empty in  *)
     let lemmas_types_infos =
       Util.Array.map2_i
 	(fun i f_constr graph ->
@@ -875,7 +875,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   i*)
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
-	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))  !evd
+	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
 	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
-- 
cgit v1.2.3