diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-22 15:36:58 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-22 15:36:58 +0000 |
| commit | 10961655cb9c09da20cfe2ecc68def3d3b7d1bb5 (patch) | |
| tree | fe435d1bd014a15e0b430cac8d7fb6bddc75f5e3 /contrib/interface | |
| parent | 8291c83620312550d1ccbe9a304fd43f35724b12 (diff) | |
Made pretyping a functor over a coercion implementation. Pretyping.Default uses the original Coercion implementation.
Updated contributions that called pretyping to use the default impl.
Also update subtac using the functor, do some renamings and add interfaces for all files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
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... |