diff options
| author | herbelin | 2004-02-13 14:58:43 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-13 14:58:43 +0000 |
| commit | 471bd570c4ab1ab9089a9cc00c16ea72ee7b2b37 (patch) | |
| tree | 55a721eaba42a0bdef12cde7168c1ff035ea8915 | |
| parent | e4834565900ccef5b0874c84657c6b4dc50947f2 (diff) | |
Bug numerotation des occurrences pour 'simpl id at n' (suite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5338 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/tacred.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 24126c0407..c11f38c8fb 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -601,7 +601,6 @@ let is_reference c = try let r = reference_of_constr c in true with _ -> false let is_head c t = - (is_reference c) & match kind_of_term t with | App (f,_) -> f = c | _ -> false @@ -852,7 +851,7 @@ let declare_red_expr s f = let reduction_of_redexp = function | Red internal -> if internal then internal_red_product else red_product | Hnf -> hnf_constr - | Simpl (Some lp) -> contextually true lp nf + | Simpl (Some (_,c as lp)) -> contextually (is_reference c) lp nf | Simpl None -> nf | Cbv f -> cbv_norm_flags (make_flag f) | Lazy f -> clos_norm_flags (make_flag f) |