diff options
Diffstat (limited to 'tactics/evar_tactics.ml')
| -rw-r--r-- | tactics/evar_tactics.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index b4a39a24..3c266c51 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_tactics.ml 11072 2008-06-08 16:13:37Z herbelin $ *) +(* $Id: evar_tactics.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Term open Util @@ -41,16 +41,16 @@ let instantiate n rawc ido gl = (match decl with (_,None,typ) -> evar_list sigma typ | _ -> error - "please be more specific : in type or value ?") + "Please be more specific: in type or value?") | InHypTypeOnly -> let (_, _, typ) = decl in evar_list sigma typ | InHypValueOnly -> (match decl with (_,Some body,_) -> evar_list sigma body - | _ -> error "not a let .. in hypothesis") in + | _ -> error "Not a defined hypothesis.") in if List.length evl < n then error "not enough uninstantiated existential variables"; - if n <= 0 then error "incorrect existential variable index"; + if n <= 0 then error "Incorrect existential variable index."; let ev,_ = destEvar (List.nth evl (n-1)) in let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in tclTHEN |