diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-15 21:01:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:18:56 +0100 |
| commit | a5feb9687819c5e7ef0db6e7b74d0e236a296674 (patch) | |
| tree | bfd809fd50c8db88f390e3d5cba22360a0c90724 /engine/uState.ml | |
| parent | d437078a4ca82f7ca6d19be5ee9452359724f9a0 (diff) | |
Separate checking univ_decls and obtaining universe binder names.
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 498d73fd3..282acb3d6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -114,6 +114,8 @@ let of_binders b = in { ctx with uctx_names = b, rmap } +let universe_binders ctx = fst ctx.uctx_names + let instantiate_variable l b v = try v := Univ.LMap.update l (Some b) !v with Not_found -> assert false @@ -291,7 +293,7 @@ let universe_context ~names ~extensible uctx = let inst = Univ.Instance.of_array inst in let ctx = Univ.UContext.make (inst, Univ.ContextSet.constraints uctx.uctx_local) in - fst uctx.uctx_names, ctx + ctx let check_implication uctx cstrs ctx = let gr = initial_graph uctx in @@ -303,14 +305,14 @@ let check_implication uctx cstrs ctx = let check_univ_decl uctx decl = let open Misctypes in - let pl, ctx = universe_context + let ctx = universe_context ~names:decl.univdecl_instance ~extensible:decl.univdecl_extensible_instance uctx in if not decl.univdecl_extensible_constraints then check_implication uctx decl.univdecl_constraints ctx; - pl, ctx + ctx let restrict ctx vars = let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in |