diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-16 14:31:24 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-16 14:31:24 +0000 |
| commit | 1c16b71834633aa11003b664757969255c0c65e5 (patch) | |
| tree | f5aa6a556a575ae75546884719ca621ec7e36fa6 /contrib | |
| parent | 6492a39fb451e3382c85937991859a25397167de (diff) | |
Export de simplest_eapply, utilisé dans la contrib interface
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9776 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -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 dc27cf983..d6dcccba6 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 - vernac_e_resolve_constr c gls + simplest_eapply c gls let rec e_trivial_fail_db db_list local_db goal = let tacl = |