diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-04 17:15:53 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-04 17:15:53 +0000 |
| commit | f9e40bd3cb4a71eadac0b4b8c9c376c39b29a981 (patch) | |
| tree | 8c2638c98ba38424893d0b93da1169036ee68156 /tactics | |
| parent | b0272a5a98d0f8dd56a56bceda6f80eb6ee70a61 (diff) | |
Instantiation of evars after instantiate (closes #1672).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10504 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/evar_tactics.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 784455ff0..a9a8da193 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -13,6 +13,7 @@ open Util open Evar_refiner open Tacmach open Tacexpr +open Refiner open Proof_type open Evd open Sign @@ -51,8 +52,11 @@ let instantiate n rawc ido gl = error "not enough uninstantiated existential variables"; if n <= 0 then error "incorrect existential variable index"; let ev,_ = destEvar (List.nth evl (n-1)) in - let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in - Refiner.tclEVARS (evars_of evd') gl + let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in + tclTHEN + (tclEVARS (evars_of evd')) + tclNORMEVAR + gl (* let pfic gls c = |