From 91c9a1294d236f55ff6fecdf1d763e7185590ea1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 26 Sep 2011 11:46:47 +0000
Subject: Moving implicit tactic support from Tacinterp to Pfedit and final
 evar resolution from Tacinterp to Pretyping (close to resolve_evars) so that
 final evar resolution can eventually be called from Tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14496 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/auto_ind_decl.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index ddf5abf03a..0a866d3b77 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -581,7 +581,7 @@ let make_bl_scheme mind =
   let nparrec = mib.mind_nparams_rec in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  [|Pfedit.build_by_tactic
+  [|Pfedit.build_by_tactic (Global.env())
     (compute_bl_goal ind lnamesparrec nparrec)
     (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|]
 
@@ -701,7 +701,7 @@ let make_lb_scheme mind =
   let nparrec = mib.mind_nparams_rec in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  [|Pfedit.build_by_tactic
+  [|Pfedit.build_by_tactic (Global.env())
     (compute_lb_goal ind lnamesparrec nparrec)
     (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|]
 
@@ -868,7 +868,7 @@ let make_eq_decidability mind =
   let nparrec = mib.mind_nparams_rec in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  [|Pfedit.build_by_tactic
+  [|Pfedit.build_by_tactic (Global.env())
     (compute_dec_goal ind lnamesparrec nparrec)
     (compute_dec_tact ind lnamesparrec nparrec)|]
 
-- 
cgit v1.2.3