diff options
Diffstat (limited to 'contrib/setoid_ring/newring.ml4')
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 40fa3a904..73ff37eda 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -754,6 +754,9 @@ let _ = add_map "field" field operations and make recursive call on the var map *) fld_cst "display_linear", (function -1|7|8|9|10|12|13->Eval|11->Rec|_->Prot); + (* Pphi_dev: evaluate polynomial and coef operations, protect + ring operations and make recursive call on the var map *) + pol_cst "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) fld_cst "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot)]);; |