diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-28 13:47:25 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:01 +0200 |
| commit | 902da7d2949464ff54dafc3fda1d44365270d2e1 (patch) | |
| tree | e8af894bb79090b316df4fbd247e09fb464bd2ac /plugins/setoid_ring/Ring_tac.v | |
| parent | 6869b22e2546b69acb74e18dc491029897ba36a3 (diff) | |
Try a new way of handling template universe levels
Diffstat (limited to 'plugins/setoid_ring/Ring_tac.v')
| -rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 1d958d09b..8bb44ecbc 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -240,23 +240,23 @@ Ltac mkPolexpr C Cst CstPow rO rI radd rmul rsub ropp rpow t fv := | (radd ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(PEadd e1 e2) + let e2 := mkP t2 in constr:(@PEadd C e1 e2) | (rmul ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(PEmul e1 e2) + let e2 := mkP t2 in constr:(@PEmul C e1 e2) | (rsub ?t1 ?t2) => fun _ => let e1 := mkP t1 in - let e2 := mkP t2 in constr:(PEsub e1 e2) + let e2 := mkP t2 in constr:(@PEsub C e1 e2) | (ropp ?t1) => fun _ => - let e1 := mkP t1 in constr:(PEopp e1) + let e1 := mkP t1 in constr:(@PEopp C e1) | (rpow ?t1 ?n) => match CstPow n with | InitialRing.NotConstant => fun _ => let p := Find_at t fv in constr:(PEX C p) - | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c) + | ?c => fun _ => let e1 := mkP t1 in constr:(@PEpow C e1 c) end | _ => fun _ => let p := Find_at t fv in constr:(PEX C p) |