diff options
| author | glondu | 2009-10-28 16:48:36 +0000 |
|---|---|---|
| committer | glondu | 2009-10-28 16:48:36 +0000 |
| commit | c14986c2fa8c8563f7da68d98b7c0b7f6ea2c9e7 (patch) | |
| tree | fc293a0e97ae8619ca629bccc14a48d62c02a925 /tactics | |
| parent | 7c151ae076fe5ebba9a2ea507f8f4a235feab9c7 (diff) | |
Remove old compatibility stuff (Tacred.nf)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 200b6deb71..9957e8a393 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -919,8 +919,8 @@ let try_delta_expand env sigma t = let simplify_args env sigma t = (* Quick hack to reduce in arguments of eq only *) match decompose_app t with - | eq, [t;c1;c2] -> applist (eq,[t;nf env sigma c1;nf env sigma c2]) - | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2]) + | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2]) + | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2]) | _ -> t let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac = |