diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-18 18:07:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-18 18:07:31 +0000 |
| commit | 2f62592cd35492c816a4672c364721781d28102a (patch) | |
| tree | f540c1c6f76baf605a7b8b11651104083e996329 | |
| parent | e46e8046dccb8d2a5d1b33b66ab24473d9d74ced (diff) | |
bug (typage avec meta)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@455 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/clenv.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 721552fad..effc8d469 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -547,8 +547,6 @@ let clenv_wtactic wt clenv = hook = wt clenv.hook } let clenv_type_of ce c = - Typing.type_of (w_env ce.hook) (w_Underlying ce.hook) c - (*** let metamap = List.map (function @@ -556,6 +554,9 @@ let clenv_type_of ce c = | (n,Cltyp typ) -> (n,typ.rebus)) (intmap_to_list ce.env) in + Retyping.get_type_of_with_meta (w_env ce.hook) (w_Underlying ce.hook) metamap c +(* Typing.type_of (w_env ce.hook) (w_Underlying ce.hook) c *) + (*** (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap (gLOB(w_hyps ce.hook)) c).uj_type ***) |