Consider OccurCheck a catchable exception.

Fix minor bug in Program wellfounded definitions.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12853 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 8 deletions

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index f51dd54099..7315326b7f 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -237,14 +237,18 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   let rel = interp_constr isevars env r 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.")
+    let error () =
+      user_err_loc (constr_loc r,
+		   "Subtac_command.build_wellfounded",
+		   my_print_constr env rel ++ str " is not an homogeneous binary relation.")
+    in
+      try
+	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
+	  | _, _ -> error ()
+      with _ -> error ()
   in
   let measure = interp_casted_constr isevars binders_env measure relargty in
   let wf_rel, wf_rel_fun, measure_fn =