Fix bug #3532, providing universe inconsistency information when a

unification fails due to that, during a conversion step.

3 files changed, 22 insertions, 12 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 616ceeabdc..f388f90057 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -324,18 +324,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
      Note: incomplete heuristic... *)
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then (
-      let evd, b = 
-	try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 
-	with Univ.UniverseInconsistency _ -> evd, false
+      let evd, e = 
+	try
+	  let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
+	    env evd term1 term2 
+	  in
+	    if b then evd, None
+	    else evd, Some (ConversionFailed (env,term1,term2))
+	with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e)
       in
-	if b then Some (evd, true)
-	else if is_ground_env evd env then Some (evd, false)
-	else None)
+	match e with
+	| None -> Some (evd, e)
+	| Some e -> 
+	  if is_ground_env evd env then Some (evd, Some e)
+	  else None)
     else None
   in
   match ground_test with
-    | Some (evd, true) -> Success evd
-    | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2))
+    | Some (evd, None) -> Success evd
+    | Some (evd, Some e) -> UnifFailure (evd,e)
     | None ->
 	(* Until pattern-unification is used consistently, use nohdbeta to not
 	   destroy beta-redexes that can be used for 1st-order unification *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 21f13a51f1..dd671f111e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1293,7 +1293,8 @@ let sigma_univ_state =
   { Reduction.compare = sigma_compare_sorts;
     Reduction.compare_instances = sigma_compare_instances }
 
-let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
+let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) 
+    env sigma x y = 
   try 
     let b, sigma = 
       let b, cstrs = 
@@ -1315,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
 	  sigma', true
   with
   | Reduction.NotConvertible -> sigma, false
-  | Univ.UniverseInconsistency _ -> sigma, false
+  | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
   | e when is_anomaly e -> error "Conversion test raised an anomaly"
     
 (********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d4f061c5be..1df2a73b2e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -268,9 +268,11 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
 
 (** [infer_fconv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
+    @raises UniverseInconsistency iff catch_incon is set to false, 
+    otherwise returns false in that case.
  *)
-val infer_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> constr -> constr -> 
-  evar_map * bool
+val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
+  env -> evar_map -> constr -> constr -> evar_map * bool
 
 (** {6 Special-Purpose Reduction Functions } *)