diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 18:30:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | fb49af8874d01871ea7ca0bd2a46d135dba27bc2 (patch) | |
| tree | 5c7ebcc651109d70bb8073a7b98174de10221648 /library | |
| parent | 8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 (diff) | |
Getting rid of AUContext abstraction breakers in Discharge.
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 4 | ||||
| -rw-r--r-- | library/lib.ml | 13 | ||||
| -rw-r--r-- | library/lib.mli | 2 |
3 files changed, 17 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index 28f108a15..154793a32 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -333,9 +333,9 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in - let sechyps,usubst,uctx = section_segment_of_mutual_inductive mind in + let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in Some (discharged_hyps kn sechyps, - Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie) + Discharge.process_inductive info repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; diff --git a/library/lib.ml b/library/lib.ml index 439f83578..a24d20c68 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -645,3 +645,16 @@ let discharge_con cst = let discharge_inductive (kn,i) = (discharge_kn kn,i) + +let discharge_abstract_universe_context (_, subst, abs_ctx) auctx = + let open Univ in + let len = LMap.cardinal subst in + let rec gen_subst i acc = + if i < 0 then acc + else + let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in + gen_subst (pred i) acc + in + let subst = gen_subst (AUContext.size auctx - 1) subst in + let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, AUContext.union abs_ctx auctx diff --git a/library/lib.mli b/library/lib.mli index 38a29f76e..f1c9bfca2 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -183,3 +183,5 @@ val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive +val discharge_abstract_universe_context : + abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t |