From 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 Dec 2013 15:08:06 +0100
Subject: Removing the need of evarmaps in constr internalization.

Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
---
 plugins/decl_mode/decl_proof_instr.ml | 3 +--
 plugins/funind/indfun.ml              | 2 +-
 plugins/funind/merge.ml               | 2 +-
 3 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index b21037d252..6e53ae6a21 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1456,8 +1456,7 @@ let do_instr raw_instr pts =
             let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
       let gl = { it=List.hd gls ; sigma=sigma; } in
       let env=  pf_env gl in
-      let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
-		 gsigma = sigma; genv = env} in
+      let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
 	interp_proof_instr (get_its_info gl) sigma env glob_instr in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3dc59b7ca7..661e5e4869 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -131,7 +131,7 @@ let rec abstract_glob_constr c = function
         (abstract_glob_constr c bl)
 
 let interp_casted_constr_with_implicits sigma env impls c  =
-  Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls
+  Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
     ~allow_patvar:false  ~ltacvars:(Id.Set.empty, Id.Set.empty) c
 
 (*
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b7c471f4ae..ac54e44cc7 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -71,7 +71,7 @@ let isVarf f x =
 let ident_global_exist id =
   try
     let ans = CRef (Libnames.Ident (Loc.ghost,id)) in
-    let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
+    let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
     true
   with e when Errors.noncritical e -> false
 
-- 
cgit v1.2.3