diff options
| author | herbelin | 2011-04-08 14:08:45 +0000 |
|---|---|---|
| committer | herbelin | 2011-04-08 14:08:45 +0000 |
| commit | e1c1d2f9de349abbcd69fe050caad674c561e91a (patch) | |
| tree | 4b707ce0cf1958eea12b8a19b68081484567f445 | |
| parent | 49fced31608d06ab672982c0a46d22b75e6f00f1 (diff) | |
Fixed "Eval ... in t" when t has still metavariables.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13968 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 938b59a9b9..088fb3b96b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1064,8 +1064,8 @@ let get_current_context_of_args = function let vernac_check_may_eval redexp glopt rc = let module P = Pretype_errors in let (sigma, env) = get_current_context_of_args glopt in + let sigma', c = interp_open_constr sigma env rc in let j = - let sigma', c = interp_open_constr sigma env rc in try Evarutil.check_evars env sigma sigma' c; Typeops.typing env c @@ -1077,10 +1077,10 @@ let vernac_check_may_eval redexp glopt rc = if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> - let redfun = fst (reduction_of_red_expr (interp_redexp env sigma r)) in + let redfun = fst (reduction_of_red_expr (interp_redexp env sigma' r)) in if !pcoq <> None - then (Option.get !pcoq).print_eval redfun env sigma rc j - else msg (print_eval redfun env sigma rc j) + then (Option.get !pcoq).print_eval redfun env sigma' rc j + else msg (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = declare_red_expr locality s (interp_redexp (Global.env()) Evd.empty r) |