diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-23 15:13:07 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-23 15:13:07 +0000 |
| commit | dc2e676c9cdedea43805c21a4b3203832a985f95 (patch) | |
| tree | 849760ef13d1460d603ce9436c244922e13a6080 /tactics/eauto.ml | |
| parent | a023ff2e48aaf7ebfb15e10dc7cdb80ab2991e8e (diff) | |
amelioration des messages d'erreurs vis a vis des evars
ajout automatique des chemins vers les sources au moment du Drop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f86262b5c..38bb22342 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -103,17 +103,9 @@ let instantiate_tac = function (fun gl -> instantiate n c gl) | _ -> invalid_arg "Instantiate called with bad arguments" -let whd_evar env sigma c = match kind_of_term c with - | IsEvar (n, cl) when Evd.in_dom sigma n & Evd.is_defined sigma n -> - Instantiate.existential_value sigma (n,cl) - | _ -> c - let normEvars gl = let sigma = project gl in - let env = pf_env gl in - let nf_evar = strong whd_evar - and simplify = nf_betaiota in - convert_concl (nf_evar env sigma (simplify env sigma (pf_concl gl))) gl + convert_concl (nf_betaiota (Evarutil.nf_evar sigma (pf_concl gl))) gl let vernac_prolog = let uncom = function |