Merge PR #7099: Stronger invariants in unification signature.

6 files changed, 59 insertions, 59 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 062136ff5..6d08f66c1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -366,13 +366,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then (
       let e =
-	try
-	  let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
-	    env evd term1 term2
-	  in
-	    if b then Success evd
-	    else UnifFailure (evd, ConversionFailed (env,term1,term2))
-	with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
+          match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with
+          | Some evd -> Success evd
+          | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))
+          | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
       in
 	match e with
 	| UnifFailure (evd, e) when not (is_ground_env evd env) -> None
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 67b7a2a40..4997d0bf0 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -25,4 +25,4 @@ val native_norm : env -> evar_map -> constr -> types -> constr
 
 (** Conversion with inference of universe constraints *)
 val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool
+  evar_map option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 92f87ab95..b2507b5f2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1082,9 +1082,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
 	      if not (occur_existential !evdref cty || occur_existential !evdref tval) then
-		let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
-		if b then (evdref := evd; cj, tval)
-		else
+                match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with
+                | Some evd -> (evdref := evd; cj, tval)
+                | None ->
 		  error_actual_type ?loc env.ExtraEnv.env !evdref cj tval 
                       (ConversionFailed (env.ExtraEnv.env,cty,tval))
 	      else user_err ?loc  (str "Cannot check cast with vm: " ++
@@ -1093,9 +1093,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
             begin
-	      let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
-	      if b then (evdref := evd; cj, tval)
-	      else
+              match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with
+              | Some evd -> (evdref := evd; cj, tval)
+              | None ->
                 error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
                   (ConversionFailed (env.ExtraEnv.env,cty,tval))
             end
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6fde86837..7fb1a0a57 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
   (** FIXME *)
   try
-    let b, sigma = 
-      let ans =
-	if pb == Reduction.CUMUL then 
+      let ans = match pb with
+      | Reduction.CUMUL ->
           EConstr.leq_constr_universes env sigma x y
-	else
+      | Reduction.CONV ->
           EConstr.eq_constr_universes env sigma x y
       in
       let ans = match ans with
@@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
         with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None
       in
       match ans with
-      | None -> false, sigma
-      | Some sigma -> true, sigma
-    in
-      if b then sigma, true
-      else
+      | Some sigma -> ans
+      | None ->
         let x = EConstr.Unsafe.to_constr x in
         let y = EConstr.Unsafe.to_constr y in
 	let sigma' = 
 	  conv_fun pb ~l2r:false sigma ts
 	    env (sigma, sigma_univ_state) x y in
-	  sigma', true
+        Some sigma'
   with
-  | Reduction.NotConvertible -> sigma, false
-  | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
+  | Reduction.NotConvertible -> None
+  | Univ.UniverseInconsistency _ when catch_incon -> None
   | e when is_anomaly e -> report_anomaly e
 
 let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ad280d9f3..9256fa7ce 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -277,13 +277,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
     otherwise returns false in that case.
  *)
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
-  env -> evar_map -> constr -> constr -> evar_map * bool
+  env -> evar_map -> constr -> constr -> evar_map option
 
 (** Conversion with inference of universe constraints *)
 val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool) -> unit
+  evar_map option) -> unit
 val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool
+  evar_map option
 
 
 (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
@@ -291,7 +291,7 @@ conversion function. Used to pretype vm and native casts. *)
 val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
     (Constr.constr, evar_map) Reduction.generic_conversion_function) ->
   ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
-  evar_map -> constr -> constr -> evar_map * bool
+  evar_map -> constr -> constr -> evar_map option
 
 (** {6 Special-Purpose Reduction Functions } *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5f7faa13e..a8a4003dc 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -579,16 +579,16 @@ let constr_cmp pb env sigma flags t u =
   in 
   match cstrs with
   | Some cstrs ->
-      begin try Evd.add_universe_constraints sigma cstrs, true
-      with Univ.UniverseInconsistency _ -> sigma, false
+      begin try Some (Evd.add_universe_constraints sigma cstrs)
+      with Univ.UniverseInconsistency _ -> None
       | Evd.UniversesDiffer -> 
 	if is_rigid_head sigma flags t then 
-          try Evd.add_universe_constraints sigma (force_eqs cstrs), true
-	  with Univ.UniverseInconsistency _ -> sigma, false
-	else sigma, false
+          try Some (Evd.add_universe_constraints sigma (force_eqs cstrs))
+          with Univ.UniverseInconsistency _ -> None
+        else None
       end
   | None ->
-    sigma, false
+    None
     
 let do_reduce ts (env, nb) sigma c =
   Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
@@ -623,9 +623,9 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM
   | None -> sigma
   | Some n ->
     if is_ground_term sigma m && is_ground_term sigma n then
-      let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in
-	if b then sigma
-	else error_cannot_unify env sigma (m,n)
+      match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with
+      | Some sigma -> sigma
+      | None -> error_cannot_unify env sigma (m,n)
     else sigma
 
 
@@ -740,11 +740,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	| Evar (evk,_ as ev), Evar (evk',_)
             when not (Evar.Set.mem evk flags.frozen_evars)
               && Evar.equal evk evk' ->
-            let sigma',b = constr_cmp cv_pb env sigma flags cM cN in
-            if b then
-	      sigma',metasubst,evarsubst
-            else
+            begin match constr_cmp cv_pb env sigma flags cM cN with
+            | Some sigma ->
+              sigma, metasubst, evarsubst
+            | None ->
 	      sigma,metasubst,((curenv,ev,cN)::evarsubst)
+            end
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
 	      && not (occur_evar sigma evk cN) ->
@@ -942,9 +943,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN =
     try canonical_projections curenvnb pb opt cM cN substn
     with ex when precatchable_exception ex ->
-    let sigma', b = constr_cmp cv_pb env sigma flags cM cN in
-      if b then (sigma', metas, evars)
-      else
+    match constr_cmp cv_pb env sigma flags cM cN with
+    | Some sigma -> (sigma, metas, evars)
+    | None ->
 	try reduce curenvnb pb opt substn cM cN
 	with ex when precatchable_exception ex ->
 	let (f1,l1) =
@@ -1001,12 +1002,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	       (* Renounce, maybe metas/evars prevents typing *) sigma
 	   else sigma
 	 in 
-	 let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in
-	    if b then Some (sigma, metasubst, evarsubst)
-	    else 
-	      if is_ground_term sigma m1 && is_ground_term sigma n1 then
-		error_cannot_unify curenv sigma (cM,cN)
-	      else None
+        match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with
+        | Some sigma ->
+          Some (sigma, metasubst, evarsubst)
+        | None ->
+          if is_ground_term sigma m1 && is_ground_term sigma n1 then
+            error_cannot_unify curenv sigma (cM,cN)
+          else None
     in
       match res with
       | Some substn -> substn
@@ -1109,11 +1111,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     then
       None
     else 
-      let sigma, b = match flags.modulo_conv_on_closed_terms with
+      let ans = match flags.modulo_conv_on_closed_terms with
 	| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
         | _ -> constr_cmp cv_pb env sigma flags m n in
-	if b then Some sigma
-	else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+      match ans with
+      | Some sigma -> ans
+      | None ->
+        if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
         | Some (cv_id, cv_k), (dl_id, dl_k) ->
           Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
         | None,(dl_id, dl_k) ->
@@ -1603,8 +1607,10 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   let merge_fun c1 c2 =
     match c1, c2 with
     | Some (evd,c1,x), Some (_,c2,_) ->
-      let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in
-      if b then Some (evd, c1, x) else raise (NotUnifiable None)
+      begin match infer_conv ~pb:CONV env evd c1 c2 with
+      | Some evd -> Some (evd, c1, x)
+      | None -> raise (NotUnifiable None)
+      end
     | Some _, None -> c1
     | None, Some _ -> c2
     | None, None -> None in
@@ -1921,10 +1927,11 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
   let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
   let typp = Typing.meta_type evd' p in
   let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
-  let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in
-  if not b then
+  match infer_conv ~pb:CUMUL env evd' predtyp typp with
+  | None ->
     error_wrong_abstraction_type env evd'
       (Evd.meta_name evd p) pred typp predtyp;
+  | Some evd' ->
   w_merge env false flags.merge_unify_flags
           (evd',[p,pred,(Conv,TypeProcessed)],[])