diff options
| author | Vincent Laporte | 2019-10-11 12:45:53 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-16 09:25:24 +0000 |
| commit | e500c71e46e6ff252455b9698addedb101662994 (patch) | |
| tree | af48fa2d87132bdae316e76f07ff8a3c11d4d6bb /engine/univGen.ml | |
| parent | 5d82451d6d6f591ad81919d8e6529cee48474b9e (diff) | |
[engine] Remove UnivGen.global_of_constr
Diffstat (limited to 'engine/univGen.ml')
| -rw-r--r-- | engine/univGen.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/engine/univGen.ml b/engine/univGen.ml index b1ed3b2694..1fe09270ba 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -82,14 +82,6 @@ let fresh_global_or_constr_instance env = function | IsConstr c -> c, ContextSet.empty | IsGlobal gr -> fresh_global_instance env gr -let global_of_constr c = - match kind c with - | Const (c, u) -> GlobRef.ConstRef c, u - | Ind (i, u) -> GlobRef.IndRef i, u - | Construct (c, u) -> GlobRef.ConstructRef c, u - | Var id -> GlobRef.VarRef id, Instance.empty - | _ -> raise Not_found - let fresh_sort_in_family = function | InSProp -> Sorts.sprop, ContextSet.empty | InProp -> Sorts.prop, ContextSet.empty |