diff options
| author | herbelin | 2007-04-28 09:34:32 +0000 |
|---|---|---|
| committer | herbelin | 2007-04-28 09:34:32 +0000 |
| commit | b61d0df2899f5de9c20ee4a2c4b79deb0714b162 (patch) | |
| tree | 6c548a7046878591025baae80b4ead8d5b349c2a /contrib/interface/blast.ml | |
| parent | 2ed87ba29db49e043062e125f3783a553d550fc4 (diff) | |
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/blast.ml')
| -rw-r--r-- | contrib/interface/blast.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index d6dcccba61..b78aa98453 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -151,7 +151,7 @@ let pp_string x = let unify_e_resolve (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false clenv' gls in - simplest_eapply c gls + Hiddentac.h_simplest_eapply c gls let rec e_trivial_fail_db db_list local_db goal = let tacl = |