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 /pretyping/clenv.ml | |
| 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 'pretyping/clenv.ml')
| -rw-r--r-- | pretyping/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 6c4dbf5ed..cb8c2cf2b 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -31,7 +31,7 @@ open Mod_subst (* *) let w_coerce env c ctyp target evd = let j = make_judge c ctyp in - let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env evd j target in + let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j target in (evd',j'.uj_val) let pf_env gls = Global.env_of_context gls.it.evar_hyps |