diff options
| author | Gaëtan Gilbert | 2018-10-10 13:37:46 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:52:52 +0200 |
| commit | 5bf063c15468bb81f0f48b583f600250cd829aee (patch) | |
| tree | 69e33cf3dd53ab18b8a359d0c2ab6f0041dc9abd /vernac | |
| parent | 404291584e861cc0f41a5585280143d2df78bd26 (diff) | |
UnivGen.constr_of_glob_univ -> Constr.mkRef
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comAssumption.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 9497f2fb03..0ef5d56d4f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -173,7 +173,7 @@ let do_assumptions kind nl l = let t = replace_vars subst t in let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 - (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u))) + (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs in subst'@subst, status' && status, next_uctx uctx) |