diff options
| author | mohring | 2001-03-06 13:48:09 +0000 |
|---|---|---|
| committer | mohring | 2001-03-06 13:48:09 +0000 |
| commit | 6da130f2ed2b8a66e7987198378cb81890c4ae03 (patch) | |
| tree | e484e88d1555b9b12078b6f85b8c777a6548b207 | |
| parent | 86e9bba21d7a5a2d9cb092476b94f1df2370cdfa (diff) | |
Modification de e_give_exact pour eviter d'echouer sur l'unification
en l'absence de variables existentielles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1431 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/eauto.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 26467421fc..9ab7ec5d64 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -15,7 +15,10 @@ open Pattern open Clenv open Auto -let e_give_exact c gl = tclTHEN (unify (pf_type_of gl c)) (exact_no_check c) gl +let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in + if occur_existential t1 or occur_existential t2 then + tclTHEN (unify t1) (exact_no_check c) gl + else exact_no_check c gl let assumption id = e_give_exact (mkVar id) |