diff options
| author | Matthieu Sozeau | 2014-06-23 15:59:03 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-23 15:59:03 +0200 |
| commit | e2b64c6df6e59dda27b3b19ca8bde19c2bdf35e2 (patch) | |
| tree | 3b5dd3d9e6d487ef69f8136884b6b07cf98f12ed /tactics/eauto.ml4 | |
| parent | db37c9f3f32ae7a2abcd5e1a3f6239eddb5e1768 (diff) | |
Oops, I fixed the .ml's
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index fd5310e040..bc3ad026cb 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -545,10 +545,12 @@ let autounfold_one db cl gl = let (ids, csts) = Hint_db.unfolds db in (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db in - let did, c' = unfold_head (pf_env gl) st (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) in + let did, c' = unfold_head (pf_env gl) st + (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) + in if did then match cl with - | Some hyp -> change_in_hyp None c' hyp gl + | Some hyp -> change_in_hyp None (fun env sigma -> sigma, c') hyp gl | None -> convert_concl_no_check c' DEFAULTcast gl else tclFAIL 0 (str "Nothing to unfold") gl |