diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-10 16:56:29 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-10 16:56:29 +0000 |
| commit | 9e860c5a4c318c6ca5e234c90716534f2682be00 (patch) | |
| tree | 5c9afa57cb9312076f7d91c57a25aec1b02fa32a /plugins/setoid_ring/Field_tac.v | |
| parent | 0dcc3068fe5e93ab5583540850c4c2caebc809d2 (diff) | |
bug in field_simplify_eq in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12729 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/setoid_ring/Field_tac.v')
| -rw-r--r-- | plugins/setoid_ring/Field_tac.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index 7aff8e0cb..9d82d1fd5 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -361,7 +361,7 @@ Tactic Notation (at level 0) "field_simplify_eq" := Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" := let G := Get_goal in - field_lookup FIELD_SIMPL [lH] G. + field_lookup (PackField FIELD_SIMPL) [lH] G. (* Same as FIELD_SIMPL but in hypothesis *) @@ -396,7 +396,7 @@ Ltac Field_simplify_eq n FLD lH := Ltac FIELD_SIMPL_EQ FLD lH rl := get_FldPre FLD (); Field_simplify_eq Ring_tac.ring_subst_niter FLD lH; - get_FldPost(). + get_FldPost FLD (). Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) := let t := type of H in |