diff options
| author | notin | 2007-04-26 14:42:38 +0000 |
|---|---|---|
| committer | notin | 2007-04-26 14:42:38 +0000 |
| commit | c900915e6e7100c9b6802d2e5641e67fa3f7ecb0 (patch) | |
| tree | b199615fb26b670de06543fb560f844f8604ce19 | |
| 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
| -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 b395c0fd99..f0e2fef687 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 |