From 2b04a76fca80b7357a7ba40322f4c001d4e12cb4 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 8 Apr 2009 20:10:07 +0000 Subject: Fix bug #2083 for good: verify that the measure and relation are well-formed before doing anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12070 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/subtac/subtac_command.ml | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 6d2902c619..bf402c24c1 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -238,15 +238,25 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel = interp_constr isevars env r in - let measure = interp_constr isevars binders_env measure in - let measure_ty = type_of binders_env !isevars measure in + let relty = type_of env !isevars rel in + let relargty = + let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in + match ctx, kind_of_term ar with + | [(_, None, t); (_, None, u)], Sort (Prop Null) + when Reductionops.is_conv env !isevars t u -> t + | _, _ -> + user_err_loc (constr_loc r, + "Subtac_command.build_wellfounded", + my_print_constr env rel ++ str " is not an homogeneous binary relation.") + in + let measure = interp_casted_constr isevars binders_env measure relargty in let wf_rel, wf_rel_fun, measure_fn = let measure_body, measure = it_mkLambda_or_LetIn measure letbinders, it_mkLambda_or_LetIn measure binders in let comb = constr_of_global (Lazy.force measure_on_R_ref) in - let wf_rel = mkApp (comb, [| argtyp; measure_ty; rel; measure |]) in + let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in let wf_rel_fun x y = mkApp (rel, [| subst1 x measure_body; subst1 y measure_body |]) -- cgit v1.2.3