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 /contrib/first-order | |
| 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/first-order')
| -rw-r--r-- | contrib/first-order/instances.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 04852da664..8eeb8b642d 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -130,7 +130,7 @@ let mk_open_instance id gl m t= RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1) | _-> anomaly "can't happen" in let ntt=try - Pretyping.understand evmap env (raux m rawt) + Pretyping.Default.understand evmap env (raux m rawt) with _ -> error "Untypable instance, maybe higher-order non-prenex quantification" in Sign.decompose_lam_n_assum m ntt |