diff options
| author | Matthieu Sozeau | 2014-03-25 18:29:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:58 +0200 |
| commit | 62fb849cf9410ddc2d9f355570f4fb859f3044c3 (patch) | |
| tree | 2f350ca302a46e18840638d20e7ff89beaf2b1f0 /toplevel | |
| parent | ca318cd0d21ce157a3042b600ded99df6face25e (diff) | |
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ind_tables.ml | 2 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 2 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 6 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index b406e53029..2a408e03d1 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -128,7 +128,7 @@ let define internal id c p univs = const_entry_type = None; const_entry_proj = None; const_entry_polymorphic = p; - const_entry_universes = Future.from_val (Evd.evar_context_universe_context ctx); + const_entry_universes = Evd.evar_context_universe_context ctx; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 757cdbea9d..57b428b5cd 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -122,7 +122,7 @@ let define id internal ctx c t = const_entry_type = t; const_entry_proj = None; const_entry_polymorphic = true; - const_entry_universes = Future.from_val (Evd.universe_context ctx); (* FIXME *) + const_entry_universes = Evd.universe_context ctx; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 3b33a91845..97c95bfd86 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -786,8 +786,8 @@ let rec string_of_list sep f = function (* Solve an obligation using tactics, return the corresponding proof term *) -let solve_by_tac evi t poly subst ctx = - let id = Id.of_string "H" in +let solve_by_tac name evi t poly subst ctx = + let id = name in let concl = Universes.subst_opt_univs_constr subst evi.evar_concl in (* spiwack: the status is dropped *) let (entry,_,subst) = Pfedit.build_constant_by_tactic @@ -905,7 +905,7 @@ and solve_obligation_by_tac prg obls i tac = | None -> snd (get_default_tactic ()) in let t, subst, ctx = - solve_by_tac (evar_of_obligation obl) tac + solve_by_tac obl.obl_name (evar_of_obligation obl) tac (pi2 prg.prg_kind) prg.prg_subst prg.prg_ctx in obls.(i) <- declare_obligation {prg with prg_subst = subst} obl t ctx; diff --git a/toplevel/record.ml b/toplevel/record.ml index 56493bae81..af7f364f31 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -262,7 +262,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; - const_entry_universes = Future.from_val ctx; + const_entry_universes = ctx; const_entry_proj = projinfo; const_entry_opaque = false; const_entry_inline_code = false; |