aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml4
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-10-05 22:43:56 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-10-05 22:43:56 +0000
commitdd7a12f1a2caddef510ad857f0183ae3501b05ac (patch)
tree5346794991eea35ae0b0e34840b5c7b4d8f13604 /tactics/rewrite.ml4
parent02a8749f2be324b2fe85897af17d9943dfcd08d7 (diff)
Correctly do backtracking during type class resolution even if only new
existentials are generated (at last!). The code simply keeps failure continuations and apply them if needed. Fix bottomup and topdown rewrite strategies that looped. Use auto introduction flag for typeclass instances as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12374 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/rewrite.ml4')
-rw-r--r--tactics/rewrite.ml47
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1c48988c7..0884b3462 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -460,7 +460,8 @@ let resolve_subrelation env sigma car rel rel' res =
let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars =
let evars, morph_instance, proj, sigargs, m', args, args' =
- let first = try (array_find args' (fun i b -> b <> None)) with Not_found -> raise (Invalid_argument "resolve_morphism") in
+ let first = try (array_find args' (fun i b -> b <> None))
+ with Not_found -> raise (Invalid_argument "resolve_morphism") in
let morphargs, morphobjs = array_chop first args in
let morphargs', morphobjs' = array_chop first args' in
let appm = mkApp(m, morphargs) in
@@ -741,10 +742,10 @@ module Strategies =
seq s (any s)
let bu (s : strategy) : strategy =
- fix (fun s' -> seq (choice (all_subterms s') s) (try_ s'))
+ fix (fun s' -> seq (choice (progress (all_subterms s')) s) (try_ s'))
let td (s : strategy) : strategy =
- fix (fun s' -> seq (choice s (all_subterms s')) (try_ s'))
+ fix (fun s' -> seq (choice s (progress (all_subterms s'))) (try_ s'))
let innermost (s : strategy) : strategy =
fix (fun ins -> choice (one_subterm ins) s)