diff options
| author | barras | 2006-10-04 21:24:09 +0000 |
|---|---|---|
| committer | barras | 2006-10-04 21:24:09 +0000 |
| commit | 6b630ee4a3cffe8472a0a0356b8aa383abaa51dd (patch) | |
| tree | 9353a8e86e50fdd3769a86c23fde545cd0e6ad4d | |
| parent | c7545949a5f4c229aac731e482c3bdc769863f41 (diff) | |
inefficacite de field_simplify_eq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9206 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 660a39b50a..233a32698b 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 40fa3a9041..73ff37edaf 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)]);; |