Protection contre un indice d'evar égal à 0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6015 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 1 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 8cdd119fcf..a58f615503 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -45,7 +45,9 @@ let instantiate n rawc ido gl =
 		  (match decl with 
 		       (_,Some body,_) -> evars_of wc.sigma body
 		     | _ -> error "not a let .. in  hypothesis") in
-    if List.length evl < n then error "not enough uninstantiated evars";
+    if List.length evl < n then
+      error "not enough uninstantiated existential variables";
+    if n <= 0 then error "incorrect existential variable index";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
     let wc' = w_refine ev rawc wc in
       Tacticals.tclIDTAC {gl with sigma = wc'.sigma}