diff options
| author | Matthieu Sozeau | 2014-06-10 19:27:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-11 15:42:51 +0200 |
| commit | e781fdf9a135526e67ebb014412c663d54ef9e28 (patch) | |
| tree | 578749aaabf171755af31353534014d56cdb3dad /pretyping | |
| parent | 06d4250ec3a62b74c41a4f41deb65e97962f8850 (diff) | |
In generalized rewrite, avoid retyping completely and constantly the conclusion, and results of
unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x
speedup in Ncring_polynom.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index dff1b9772f..cb6deb41cb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -318,11 +318,12 @@ let pretype_ref loc evdref env ref us = make_judge c ty let judge_of_Type evd s = - let judge s = + let evd, l = interp_universe_name evd s in + let s = Univ.Universe.make l in + let judge = { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } in - let evd, l = interp_universe_name evd s in - evd, judge (Univ.Universe.make l) + evd, judge let pretype_sort evdref = function | GProp -> judge_of_prop |