diff options
| author | msozeau | 2006-03-22 15:36:58 +0000 |
|---|---|---|
| committer | msozeau | 2006-03-22 15:36:58 +0000 |
| commit | 10961655cb9c09da20cfe2ecc68def3d3b7d1bb5 (patch) | |
| tree | fe435d1bd014a15e0b430cac8d7fb6bddc75f5e3 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 1591d43c92..0f3fa75843 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -28,7 +28,7 @@ let w_refine env ev rawc evd = let e_info = Evd.map (evars_of evd) ev in let env = Evd.evar_env e_info in let sigma,typed_c = - Pretyping.understand_tcc (evars_of evd) env + Pretyping.Default.understand_tcc (evars_of evd) env ~expected_type:e_info.evar_concl rawc in evar_define ev typed_c (evars_reset_evd sigma evd) |