diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-05-21 14:46:30 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:16 +0200 |
| commit | 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f (patch) | |
| tree | 578e5b07c936a92a5ac26d62987a4413c85a9696 /proofs/proof_global.ml | |
| parent | 4385872b2d82fbad2be84f2423802e00e9d9575f (diff) | |
Squashed commit of the following:
Except I have disabled the minimization of universes after sections as
it seems to interfere with the STM machinery causing files like
test-suite/vio/print.v to loop when processed asynchronously.
This is very peculiar and needs more investigation as the aforementioned
file does not have any sections or any universe polymorphic definitions!
commit fc785326080b9451eb4700b16ccd3f7df214e0ed
Author: Amin Timany <amintimany@gmail.com>
Date: Mon Apr 24 17:14:21 2017 +0200
Revert STL to monomorphic
commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996
Author: Amin Timany <amintimany@gmail.com>
Date: Mon Apr 24 17:02:42 2017 +0200
Try unifying universes before apply subtyping
commit ff393742c37b9241c83498e84c2274967a1a58dc
Author: Amin Timany <amintimany@gmail.com>
Date: Sun Apr 23 13:49:04 2017 +0200
Compile more of STL with universe polymorphism
commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6
Author: Amin Timany <amintimany@gmail.com>
Date: Tue Apr 18 21:26:45 2017 +0200
Made more progress on compiling the standard library
commit b8550ffcce0861794116eb3b12b84e1158c2b4f8
Author: Amin Timany <amintimany@gmail.com>
Date: Sun Apr 16 22:55:19 2017 +0200
Make more number theoretic modules monomorphic
commit 29d126d4d4910683f7e6aada2a25209151e41b10
Author: Amin Timany <amintimany@gmail.com>
Date: Fri Apr 14 16:11:48 2017 +0200
WIP more of standard library compiles
Also: Matthieu fixed a bug in rewrite system which was faulty when
introducing new morphisms (Add Morphism) command.
commit 23bc33b843f098acaba4c63c71c68f79c4641f8c
Author: Amin Timany <amintimany@gmail.com>
Date: Fri Apr 14 11:39:21 2017 +0200
WIP: more of the standard library compiles
We have implemented convertibility of constructors up-to mutual
subtyping of their corresponding inductive types. This is similar to
the behavior of template polymorphism.
commit d0abc5c50d593404fb41b98d588c3843382afd4f
Author: Amin Timany <amintimany@gmail.com>
Date: Wed Apr 12 19:02:39 2017 +0200
WIP: trying to get the standard library compile with universe polymorphism
We are trying to prune universes after section ends. Sections add a
load of universes that are not appearing in the body, type or the
constraints.
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5ec34a638..f5664aed0 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -343,8 +343,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now nf t else t in - let used_univs_body = Universes.universes_of_constr body in - let used_univs_typ = Universes.universes_of_constr typ in + let used_univs_body = Univops.universes_of_constr body in + let used_univs_typ = Univops.universes_of_constr typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in @@ -353,7 +353,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = restrict_universe_context ctx used_univs in + let ctx_body = Univops.restrict_universe_context ctx used_univs in (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in @@ -362,7 +362,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now * constraints in which we merge the ones for the body and the ones * for the typ *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = restrict_universe_context ctx used_univs in + let ctx = Univops.restrict_universe_context ctx used_univs in let univs = Univ.ContextSet.to_context ctx in (univs, typ), ((body, Univ.ContextSet.empty), eff) in |