diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1b460b060..d8e03265d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1046,7 +1046,7 @@ let mk_open_constr_value ist gl c = let mk_hyp_value ist gl c = Value.of_constr (mkVar (interp_hyp ist gl c)) let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c) -let pack_sigma (sigma,c) = {it=c;sigma=sigma} +let pack_sigma eff (sigma,c) = {it=c;sigma=sigma;eff=eff} let extend_gl_hyps { it=gl ; sigma=sigma } sign = Goal.V82.new_goal_with sigma gl sign @@ -1317,7 +1317,7 @@ and interp_letin ist gl llc u = (* Interprets the Match Context expressions *) and interp_match_goal ist goal lz lr lmr = let (gl,sigma) = Goal.V82.nf_evar (project goal) (sig_it goal) in - let goal = { it = gl ; sigma = sigma } in + let goal = { it = gl ; sigma = sigma; eff = sig_eff goal } in let hyps = pf_hyps goal in let hyps = if lr then List.rev hyps else hyps in let concl = pf_concl goal in @@ -1457,11 +1457,11 @@ and interp_genarg ist gl x = (snd (out_gen (glbwit (wit_open_constr_gen casted)) x))) | ConstrWithBindingsArgType -> in_gen (topwit wit_constr_with_bindings) - (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl) + (pack_sigma (sig_eff gl) (interp_constr_with_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_constr_with_bindings) x))) | BindingsArgType -> in_gen (topwit wit_bindings) - (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x))) + (pack_sigma (sig_eff gl) (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x))) | ListArgType ConstrArgType -> let (sigma,v) = interp_genarg_constr_list ist gl x in evdref := sigma; |