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 /tactics/elimschemes.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 'tactics/elimschemes.ml')
-rw-r--r-- | tactics/elimschemes.ml | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 466b1350d..8d8e19811 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -80,30 +80,30 @@ let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) -let ind_scheme_kind_from_type = - declare_individual_scheme_object "_ind_nodep" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp) - -let ind_scheme_kind_from_prop = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" - (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp) - -let ind_dep_scheme_kind_from_type = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp) +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) -let rec_scheme_kind_from_type = - declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) - let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) +let ind_scheme_kind_from_type = + declare_individual_scheme_object "_ind_nodep" + (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp) + +let ind_dep_scheme_kind_from_type = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" + (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp) + +let ind_scheme_kind_from_prop = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" + (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp) + (* Case analysis *) let build_case_analysis_scheme_in_type dep sort ind = |