diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /tactics/evar_tactics.ml | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
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 |