diff options
| author | herbelin | 2000-07-28 13:28:09 +0000 |
|---|---|---|
| committer | herbelin | 2000-07-28 13:28:09 +0000 |
| commit | 89a3416f68bddad29e80ed7d4f93b4a5ef418bd7 (patch) | |
| tree | bde5b9b4eb8f82b6a027d7156fcf91055eeeaac2 | |
| parent | 0aa70be388ced06a8471ff9e53408b2b9770f2f7 (diff) | |
messages d'erreur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@576 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0beab3f7a1..2c418bbae8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -363,7 +363,7 @@ let rec intros_until s g = with UserError ("Term not reducible",_) -> errorlabstrm "Intros" [<'sTR "No such hypothesis in current goal"; - 'sTR "even after head-reduction" >] + 'sTR " even after head-reduction" >] let rec intros_until_n n g = match pf_lookup_index_as_renamed (pf_concl g) n with @@ -374,7 +374,7 @@ let rec intros_until_n n g = with UserError ("Term not reducible",_) -> errorlabstrm "Intros" [<'sTR "No such hypothesis in current goal"; - 'sTR "even after head-reduction" >] + 'sTR " even after head-reduction" >] let dyn_intros_until = function | [Identifier id] -> intros_until id |