diff options
Diffstat (limited to 'contrib/setoid_ring')
-rw-r--r-- | contrib/setoid_ring/Field_tac.v | 2 | ||||
-rw-r--r-- | contrib/setoid_ring/newring.ml4 | 3 |
2 files changed, 4 insertions, 1 deletions
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index 660a39b50..233a32698 100644 --- a/contrib/setoid_ring/Field_tac.v +++ b/contrib/setoid_ring/Field_tac.v @@ -156,6 +156,6 @@ Ltac Make_field_simplify_eq_tac lemma Cond_lemma req Cst_tac := let Main radd rmul rsub ropp rdiv rinv C := let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in - let Simpl := (unfold Pphi_dev; simpl) in + let Simpl := (protect_fv "field") in Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in ParseFieldComponents lemma req Main. 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)]);; |