diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-01 18:49:15 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-01 18:49:15 +0000 |
| commit | 8cfa56ae58f63e1e1ce046f79017ee90e9adab6d (patch) | |
| tree | 90fdef185d48d0635e800333dfacd10406ef3dd5 /contrib | |
| parent | d67a33093ae171ab7efec8a90ea7fce924d3dc10 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 14 |
1 files 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 = |