From 6b630ee4a3cffe8472a0a0356b8aa383abaa51dd Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 4 Oct 2006 21:24:09 +0000 Subject: inefficacite de field_simplify_eq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9206 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/setoid_ring/newring.ml4 | 3 +++ 1 file changed, 3 insertions(+) (limited to 'contrib/setoid_ring/newring.ml4') 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)]);; -- cgit v1.2.3