diff options
| author | Gaëtan Gilbert | 2019-01-30 14:39:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-17 15:44:30 +0100 |
| commit | a9f0fd89cf3bb4b728eb451572a96f8599211380 (patch) | |
| tree | 577b7330af67793041cfaba8414005f93fc49c88 /tactics | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
Separate variance and universe fields in inductives.
I think the usage looks cleaner this way.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 4 | ||||
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 2 | ||||
| -rw-r--r-- | tactics/leminv.ml | 4 |
4 files changed, 5 insertions, 7 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index c3e3a62e26..7a61deba0c 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -162,8 +162,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let cst = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with - | Entries.Monomorphic_const_entry _ -> EInstance.empty - | Entries.Polymorphic_const_entry (_, ctx) -> + | Entries.Monomorphic_entry _ -> EInstance.empty + | Entries.Polymorphic_entry (_, ctx) -> (* We mimick what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 571ad9d160..c1f6365f5d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1309,7 +1309,7 @@ let project_hint ~poly pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in - let ctx = Evd.const_univ_entry ~poly sigma in + let ctx = Evd.univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index a67f5f6d6e..d1b77f3758 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -121,7 +121,7 @@ let define internal id c poly univs = let id = compute_name internal id in let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in - let univs = UState.const_univ_entry ~poly ctx in + let univs = UState.univ_entry ~poly ctx in let entry = { const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 48997163de..335f3c74ff 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -237,9 +237,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in - let univs = - Evd.const_univ_entry ~poly sigma - in + let univs = Evd.univ_entry ~poly sigma in let entry = definition_entry ~univs invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () |