From 9e860c5a4c318c6ca5e234c90716534f2682be00 Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 10 Feb 2010 16:56:29 +0000 Subject: bug in field_simplify_eq in git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12729 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/setoid_ring/Field_tac.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/setoid_ring/Field_tac.v') 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 -- cgit v1.2.3