diff options
| author | herbelin | 2009-03-16 08:18:53 +0000 |
|---|---|---|
| committer | herbelin | 2009-03-16 08:18:53 +0000 |
| commit | 171c73b40b985f604e4d6c1529fb28d1dfa8e300 (patch) | |
| tree | ca36754a96d68fcedf329fb5217d41c171c30008 /contrib/firstorder | |
| parent | 208f162ab68d00488248ee052947592dd23d5d52 (diff) | |
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
Diffstat (limited to 'contrib/firstorder')
| -rw-r--r-- | contrib/firstorder/g_ground.ml4 | 2 | ||||
| -rw-r--r-- | contrib/firstorder/rules.ml | 7 |
2 files changed, 4 insertions, 5 deletions
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)) |