diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-21 19:33:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-21 19:33:03 +0200 |
| commit | b1791fe718eae95897d2dbd160b05285c6df239c (patch) | |
| tree | a6fa303116109888dbfe4451595a2680b1e759a3 | |
| parent | 00808a1fa05e34fee36b8dfff4e7c72943b22c23 (diff) | |
Do not recompute the whole evar naming environment in GProd intepretation.
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e7f87c5f7..f46674003 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -804,8 +804,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = pretype_type empty_valcon env evdref lvar c2 in { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = (name,j.utj_val) in - let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in + let var = LocalAssum (name, j.utj_val) in + let env' = push_rel var env in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in |