diff options
author | 2009-10-05 22:43:56 +0000 | |
---|---|---|
committer | 2009-10-05 22:43:56 +0000 | |
commit | dd7a12f1a2caddef510ad857f0183ae3501b05ac (patch) | |
tree | 5346794991eea35ae0b0e34840b5c7b4d8f13604 /tactics/rewrite.ml4 | |
parent | 02a8749f2be324b2fe85897af17d9943dfcd08d7 (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.ml4 | 7 |
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) |