From 171c73b40b985f604e4d6c1529fb28d1dfa8e300 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 16 Mar 2009 08:18:53 +0000
Subject: Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H
 at 4" now works correctly, "unfold foo at 4 in H at 3" now fails correctly,
 etc.). The terminology for clauses (though I don't find the term "clause"
 very intuitive after all) is mostly preserved except for "simple_clause"
 which becomes a light form of "clause" instead of being an atom of clause
 (what played the role of "simple_clause" is now called "goal_location" -
 better names are welcome). Main changes are in tacticals.ml and tactics.ml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/firstorder/g_ground.ml4 | 2 +-
 contrib/firstorder/rules.ml     | 7 +++----
 2 files changed, 4 insertions(+), 5 deletions(-)

(limited to 'contrib/firstorder')

diff --git a/contrib/firstorder/g_ground.ml4 b/contrib/firstorder/g_ground.ml4
index 3ee1db14c9..d7c5b66ae7 100644
--- a/contrib/firstorder/g_ground.ml4
+++ b/contrib/firstorder/g_ground.ml4
@@ -89,7 +89,7 @@ let defined_connectives=lazy
    [],EvalConstRef (destConst (constant "iff"))]
 
 let normalize_evaluables=
-  onAllClauses
+  onAllHypsAndConcl
     (function 
 	 None->unfold_in_concl (Lazy.force defined_connectives)
        | Some id-> 
diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml
index 91607ec40f..fc31ee6fc7 100644
--- a/contrib/firstorder/rules.ml
+++ b/contrib/firstorder/rules.ml
@@ -208,9 +208,8 @@ let defined_connectives=lazy
    all_occurrences,EvalConstRef (destConst (constant "iff"))]
 
 let normalize_evaluables=
-  onAllClauses
+  onAllHypsAndConcl
     (function 
 	 None->unfold_in_concl (Lazy.force defined_connectives)
-       | Some ((_,id),_)-> 
-	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   ((Rawterm.all_occurrences_expr,id),InHypTypeOnly))
+       | Some id -> 
+	   unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
-- 
cgit v1.2.3