From 8cfa56ae58f63e1e1ce046f79017ee90e9adab6d Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 1 Feb 2006 18:49:15 +0000 Subject: protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7973 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/setoid_ring/newring.ml4 | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 0b0362a3b..48f9ec51a 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -177,11 +177,15 @@ let arg_map = [mk_cst [contrib_name;"BinList"] "cons",(function -1->Eval|2->Rec|_->Prot); mk_cst [contrib_name;"BinList"] "nil", (function -1->Eval|_ -> 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 *) - pol_cst "PEeval", (function -1|7|9->Eval|8->Rec|_->Prot)];; + ring operations and make recursive call on morphism and var map *) + pol_cst "Pphi_dev", (function -1|6|7|8|11->Eval|9|10->Rec|_->Prot); + (* PEeval: evaluate polynomial, protect ring operations + and make recursive call on morphism and var map *) + pol_cst "PEeval", (function -1|9->Eval|7|8->Rec|_->Prot); + (* Do not evaluate ring operations... *) + ring_constant "gen_phiZ", (function -1|6->Eval|_->Prot); + ring_constant "gen_phiN", (function -1|5->Eval|_->Prot); +];; (* Equality: do not evaluate but make recursive call on both sides *) let is_ring_thm req = -- cgit v1.2.3