diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-14 12:08:51 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-14 12:08:51 +0000 |
| commit | fe7a84374e90d090806f6a970c425d304c2e150f (patch) | |
| tree | 4ad88ab506a07dcc964987991047a176cb142255 /tactics | |
| parent | 599b4bb3fc6c9ad712bc280c0f01a2c2918b15e2 (diff) | |
evar tactic bugfix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6105 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/evar_tactics.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index f2db79d1a..d65b1f3eb 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -15,6 +15,8 @@ open Tacmach open Tacexpr open Proof_type open Evd +open Sign +open Termops (* The instantiate tactic *) @@ -32,7 +34,7 @@ let instantiate n rawc ido gl = match ido with ConclLocation () -> evars_of wc.sigma gl.it.evar_concl | HypLocation (id,hloc) -> - let decl = Sign.lookup_named id gl.it.evar_hyps in + let decl = lookup_named id gl.it.evar_hyps in match hloc with InHyp -> (match decl with @@ -70,4 +72,7 @@ let let_evar nam typ gls = let evd = Evarutil.create_evar_defs gls.sigma in let evd' = Unification.w_Declare (pf_env gls) sp typ evd in let ngls = {gls with sigma = Evarutil.evars_of evd'} in - Tactics.forward true nam (mkEvar(sp,[||])) ngls + let args = Array.of_list + (List.map mkVar (ids_of_named_context (pf_hyps gls))) in + Tactics.forward true nam (mkEvar(sp,args)) ngls + |