diff options
| -rw-r--r-- | proofs/clenvtac.ml | 3 | ||||
| -rw-r--r-- | proofs/logic.ml | 3 | ||||
| -rw-r--r-- | proofs/logic.mli | 1 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 5 |
4 files changed, 10 insertions, 2 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 5c204c8bb..f368ed379 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -54,7 +54,8 @@ let clenv_cast_meta clenv = (match Evd.find_meta clenv.evd mv with | Clval (_,(body,_),_) -> body.rebus | Cltyp (_,typ) -> - assert (not (occur_meta typ.rebus)); + if occur_meta typ.rebus then + raise (RefinerError (MetaInType typ.rebus)); mkCast (mkMeta mv, DEFAULTcast, typ.rebus)) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) | Case(ci,p,c,br) -> mkCase (ci, crec p, crec_hd c, Array.map crec br) diff --git a/proofs/logic.ml b/proofs/logic.ml index c358de9ba..0368e9744 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -37,6 +37,7 @@ type refiner_error = | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr + | MetaInType of constr (* Errors raised by the tactics *) | IntroNeedsProduct @@ -251,7 +252,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = match kind_of_term trm with | Meta _ -> if !check && occur_meta conclty then - anomaly "refine called with a dependent meta"; + raise (RefinerError (MetaInType conclty)); (mk_goal hyps (nf_betaiota conclty))::goalacc, conclty | Cast (t,_, ty) -> diff --git a/proofs/logic.mli b/proofs/logic.mli index 88e77fd7b..8bc48ed54 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -54,6 +54,7 @@ type refiner_error = | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr + | MetaInType of constr (*i Errors raised by the tactics i*) | IntroNeedsProduct diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index d6ce01bbc..f253a0a7a 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -576,6 +576,10 @@ let explain_non_linear_proof c = str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ spc () ++ str "because a metavariable has several occurrences." +let explain_meta_in_type c = + str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++ + str " of another meta" + let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t @@ -584,6 +588,7 @@ let explain_refiner_error = function | IntroNeedsProduct -> explain_intro_needs_product () | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp | NonLinearProof c -> explain_non_linear_proof c + | MetaInType c -> explain_meta_in_type c (* Inductive errors *) |