diff options
| author | Gaëtan Gilbert | 2020-01-17 17:28:50 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-27 13:54:43 +0100 |
| commit | f011a88bd4be4797617741d6829d2530bc29ebdf (patch) | |
| tree | 42baae9f5d4d4e9f27233649e5d4920ada0b0617 /tactics | |
| parent | 506b35913103c17e4d27663aa0f977452d5815b0 (diff) | |
schemes: use rigid universes
so for instance
~~~coq
Set Printing All. Set Printing Universes.
Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
Lemma bla@{u v|u < v} : foo@{u v} -> False.
Proof. induction 1. Qed.
~~~
works.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elimschemes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index d6fda00ad8..6cdb24965d 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -49,14 +49,14 @@ let optimize_non_type_induction_scheme kind dep sort ind = let sigma = Evd.minimize_universes sigma in (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma) else - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in (c, Evd.evar_universe_context sigma) let build_induction_scheme_in_type dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma |