diff options
| -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 784455ff0d..a9a8da1938 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 = |