diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-17 14:56:04 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-17 14:56:04 +0000 |
commit | 8ac929ea128f1f7353b3f4d532b642e769542e55 (patch) | |
tree | b77b28d76ae301b4af81e18309bff869625c6f99 /proofs/evar_refiner.ml | |
parent | 97fc36f552bfd9731ac47716faf2b02d4555eb07 (diff) |
Added propagation of evars unification failure reasons for better
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/evar_refiner.ml')
-rw-r--r-- | proofs/evar_refiner.ml | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 71a07326f..92ee55e43 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -11,6 +11,7 @@ open Util open Names open Evd open Evarutil +open Evarsolve (******************************************) (* Instantiation of existential variables *) @@ -23,15 +24,17 @@ let depends_on_evar evk _ (pbty,_,t1,t2) = with NoHeadEvar -> false let define_and_solve_constraints evk c evd = - try - let evd = define evk c evd in - let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in - fst (List.fold_left - (fun (evd,b as p) (pbty,env,t1,t2) -> - if b then Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 else p) (evd,true) - pbs) - with e when Pretype_errors.precatchable_exception e -> - error "Instance does not satisfy constraints." + let evd = define evk c evd in + let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in + match + List.fold_left + (fun p (pbty,env,t1,t2) -> match p with + | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 + | UnifFailure _ as x -> x) (Success evd) + pbs + with + | Success evd -> evd + | UnifFailure _ -> error "Instance does not satisfy the constraints." let w_refine (evk,evi) (ltac_var,rawc) sigma = if Evd.is_defined sigma evk then |