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 /engine/univGen.ml | |
| parent | 404291584e861cc0f41a5585280143d2df78bd26 (diff) | |
UnivGen.constr_of_glob_univ -> Constr.mkRef
Diffstat (limited to 'engine/univGen.ml')
| -rw-r--r-- | engine/univGen.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/engine/univGen.ml b/engine/univGen.ml index 64789cb808..4cdcfd9730 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -105,12 +105,7 @@ let constr_of_global gr = str " would forget universes.") else c -let constr_of_global_univ (gr,u) = - match gr with - | VarRef id -> mkVar id - | ConstRef sp -> mkConstU (sp,u) - | ConstructRef sp -> mkConstructU (sp,u) - | IndRef sp -> mkIndU (sp,u) +let constr_of_global_univ = mkRef let fresh_global_or_constr_instance env = function | IsConstr c -> c, ContextSet.empty |