From a5c1b866a6d7f096d6fcb30bd63036436cfd36f8 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Wed, 18 Apr 2012 14:47:43 +0000
Subject: Corrects a (very) longstanding bug of tactics. As is were, tactic
 expecting constr as argument (rather than openconstr) assumed that the
 evar_map output by pretyping was irrelevant as the final constr didn't have
 any evars. However, if said constr was defined using pre-existing evars from
 the context, the evars may be instantiated by pretyping, hence dropping the
 output evar_map led to inconsistent proof terms.

This fixes bug #2739 ( https://coq.inria.fr/bugs/show_bug.cgi?id=2739 ).
Thanks Arthur for noticing it.

Note: change still has the bug, because more serious issues interfered with
my fix.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15207 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/decl_mode/g_decl_mode.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index fd98d54579..045678f0c2 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -111,6 +111,7 @@ let _ = Tacinterp.add_interp_genarg "proof_instr"
       (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x))
   end,
   begin fun ist gl x -> (* declares the interpretation function *)
+    Tacmach.project gl ,
     Genarg.in_gen wit_proof_instr 
       (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x))
   end,
-- 
cgit v1.2.3