diff options
| author | Hugo Herbelin | 2014-10-21 11:07:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-21 12:15:45 +0200 |
| commit | be0121602ff9fb3200cafead25e325617164038a (patch) | |
| tree | 34f5363c83df0ff7c852e4e619038187a3408948 | |
| parent | da462f8a2b59a3d5ddd9f09add8a75f8e2624c9a (diff) | |
Continuing experimental printing of the signature of open evars in
Check (see cfff8f8a327) [printing only visible evars, not the ones
corresponding to unrelated open goals + fixing bug on wrong sigma and
on evar_info normalization].
| -rw-r--r-- | toplevel/vernacentries.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a41569377f..816912be40 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1481,16 +1481,20 @@ let vernac_check_may_eval redexp glopt rc = let c = nf c in let j = try - Evarutil.check_evars env Evd.empty sigma' c; + Evarutil.check_evars env sigma sigma' c; Arguments_renaming.rename_typing env c with Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) -> Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in match redexp with | None -> - let l = Evarutil.non_instantiated sigma' in - let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma j.Environ.uj_type } in + let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in + let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in msg_notice (print_judgment env sigma' j ++ - (if l != Evar.Map.empty then (fnl () ++ str "where" ++ fnl () ++ pr_evars sigma' l) else mt ()) ++ + (if l != Evar.Set.empty then + let l = Evar.Set.fold (fun ev -> Evar.Map.add ev (Evarutil.nf_evar_info sigma' (Evd.find sigma' ev))) l Evar.Map.empty in + (fnl () ++ str "where" ++ fnl () ++ pr_evars sigma' l) + else + mt ()) ++ Printer.pr_universe_ctx uctx) | Some r -> Tacintern.dump_glob_red_expr r; |