diff options
author | 2007-04-26 14:42:38 +0000 | |
---|---|---|
committer | 2007-04-26 14:42:38 +0000 | |
commit | c900915e6e7100c9b6802d2e5641e67fa3f7ecb0 (patch) | |
tree | b199615fb26b670de06543fb560f844f8604ce19 /proofs | |
parent | ea1eaa9b152b73652f417e02bd469e5b289cec47 (diff) |
Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et uniformisation des messages d'erreur wrt instantiate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9798 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/evar_refiner.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index b395c0fd9..f0e2fef68 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -41,12 +41,16 @@ let instantiate_pf_com n com pfts = let gls = top_goal_of_pftreestate pfts in let sigma = gls.sigma in let (sp,evi) (* as evc *) = - try - List.nth (Evarutil.non_instantiated sigma) (n-1) - with Failure _ -> - error "not so many uninstantiated existential variables" in + let evl = Evarutil.non_instantiated sigma in + if (n <= 0) then + error "incorrect existential variable index" + else if List.length evl < n then + error "not so many uninstantiated existential variables" + else + List.nth evl (n-1) + in let env = Evd.evar_env evi in let rawc = Constrintern.intern_constr sigma env com in let evd = create_evar_defs sigma in let evd' = w_refine sp rawc evd in - change_constraints_pftreestate (evars_of evd') pfts + change_constraints_pftreestate (evars_of evd') pfts |