diff options
| author |  Matěj Grabovský <mgrabovsky@yahoo.com> | 2015-02-11 10:04:20 +0100 |
|---|---|---|
| committer |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-11 18:06:23 +0100 |
| commit | 34c7ef490d26e67ad1545dba65db7080744ffbe0 (patch) | |
| tree | 8bce5715dc1fff6c3a1d3f2cfd7a37da51430a1c /tactics | |
| parent | 4261cc40270ee8abfa8ced859a8fb0b209cc78a8 (diff) | |
Missing space in error message
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9265328a4..a298bba97 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -425,7 +425,7 @@ let pf_reduce_decl redfun where (id,c,ty) gl = match c with | None -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str "has no value."); + errorlabstrm "" (pr_id id ++ str " has no value."); (id,None,redfun' ty) | Some b -> let b' = if where != InHypTypeOnly then redfun' b else b in @@ -522,7 +522,7 @@ let pf_e_reduce_decl redfun where (id,c,ty) gl = match c with | None -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str "has no value."); + errorlabstrm "" (pr_id id ++ str " has no value."); let sigma, ty' = redfun sigma ty in sigma, (id,None,ty') | Some b -> @@ -565,7 +565,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env match c with | None -> if where == InHypValueOnly then - errorlabstrm "" (pr_id id ++ str "has no value."); + errorlabstrm "" (pr_id id ++ str " has no value."); let sigma',ty' = redfun false env sigma ty in sigma', (id,None,ty') | Some b -> |