diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml4 | 2 | ||||
| -rw-r--r-- | contrib/interface/pbp.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index cb43a45ed..8fcdb5d90 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -400,7 +400,7 @@ let inspect n = add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_sp sp)) - (Pretyping.understand Evd.empty (Global.env()) + (Pretyping.Default.understand Evd.empty (Global.env()) (RRef(dummy_loc, IndRef(kn,0)))) | _ -> failwith ("unexpected value 1 for "^ (string_of_id (basename (fst oname))))) diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 19b06a30d..d2f71bfc2 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -34,7 +34,7 @@ let get_hyp_by_name g name = let evd = project g in let env = pf_env g in try (let judgment = - Pretyping.understand_judgment + Pretyping.Default.understand_judgment evd env (RVar(zz, name)) in ("hyp",judgment.uj_type)) (* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up... |