diff options
| author | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
| commit | a59574c8eb4bdda60e4bdd6197e8a32574985588 (patch) | |
| tree | e15e1a0f78d23cd263726d725c93a5e6ce453465 /pretyping/evarconv.ml | |
| parent | f8d6c322783577b31cf55f8b55568ac56104202b (diff) | |
| parent | a9f0fd89cf3bb4b728eb451572a96f8599211380 (diff) | |
Merge PR #9439: Separate variance and universe fields in inductives.
Ack-by: ppedrot
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aa30ed8d2e..bb163ddaee 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -468,17 +468,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let u = EInstance.kind evd u and u' = EInstance.kind evd u' in let mind = Environ.lookup_mind mi env in let open Declarations in - begin match mind.mind_universes with - | Monomorphic_ind _ -> assert false - | Polymorphic_ind _ -> check_strict evd u u' - | Cumulative_ind cumi -> + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> let nparamsaplied = Stack.args_size sk in let nparamsaplied' = Stack.args_size sk' in let needed = Reduction.inductive_cumulativity_arguments (mind,i) in if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) then check_strict evd u u' else - compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u' + compare_cumulative_instances evd variances u u' end | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') @@ -488,10 +487,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let u = EInstance.kind evd u and u' = EInstance.kind evd u' in let mind = Environ.lookup_mind mi env in let open Declarations in - begin match mind.mind_universes with - | Monomorphic_ind _ -> assert false - | Polymorphic_ind _ -> check_strict evd u u' - | Cumulative_ind cumi -> + begin match mind.mind_variance with + | None -> check_strict evd u u' + | Some variances -> let nparamsaplied = Stack.args_size sk in let nparamsaplied' = Stack.args_size sk' in let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in |