diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-05 21:36:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:23:53 +0100 |
| commit | b7fd585b89ac5e0b7770f52739c33fe179f2eed8 (patch) | |
| tree | 83ab6fe2ccecb503691c9842ba7eec27690ad975 /pretyping/typing.ml | |
| parent | 147afe827dc83602cc160a8b1357e84ecea910ff (diff) | |
Evarsolve API using EConstr.
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index db31541cd..1dcb5f945 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -309,7 +309,7 @@ let type_of ?(refresh=false) env evd c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type + Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type) else !evdref, j.uj_type let e_type_of ?(refresh=false) env evdref c = @@ -317,7 +317,7 @@ let e_type_of ?(refresh=false) env evdref c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in + let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type) in let () = evdref := evd in c else j.uj_type |