Stronger invariants in unification signature.

We use an option type instead of returning a pair with a boolean. Indeed, the
boolean being true was always indicating that the returned value was unchanged.
The previous API was somewhat error-prone, and I don't understand why it was
designed this way in the first place.

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

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

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

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 ->

pretyping/reductionops.mli

@@ -277,21 +277,21 @@ 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
 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 } *)
 

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)],[])
 

proofs/logic.ml

@@ -309,9 +309,10 @@ let check_meta_variables env sigma c =
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
-      if b then evm 
-      else raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
+    let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+    match ans with
+    | Some evm -> evm
+    | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
   else sigma
 
 exception Stop of EConstr.t list

tactics/tactics.ml

@@ -158,9 +158,9 @@ let convert_concl ?(check=true) ty k =
       let sigma =
         if check then begin
           ignore (Typing.unsafe_type_of env sigma ty);
-          let sigma,b = Reductionops.infer_conv env sigma ty conclty in
-          if not b then error "Not convertible.";
-          sigma
+          match Reductionops.infer_conv env sigma ty conclty with
+          | None -> error "Not convertible."
+          | Some sigma -> sigma
         end else sigma in
       let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
       let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
@@ -186,11 +186,10 @@ let convert_hyp_no_check = convert_hyp ~check:false
 
 let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
-    try
-      let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in
-      if b then Proofview.Unsafe.tclEVARS sigma
-      else Tacticals.New.tclFAIL 0 (str "Not convertible")
-    with (* Reduction.NotConvertible *) _ ->
+    match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
+    | Some sigma -> Proofview.Unsafe.tclEVARS sigma
+    | None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
+    | exception _ ->
       (** FIXME: Sometimes an anomaly is raised from conversion *)
       Tacticals.New.tclFAIL 0 (str "Not convertible")
 end
@@ -796,15 +795,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
     let t2 = Retyping.get_type_of env sigma origc in
     let sigma, t2 = Evarsolve.refresh_universes
 		      ~onlyalg:true (Some false) env sigma t2 in
-    let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
-    if not b then
+    match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with
+    | None ->
       if
         isSort sigma (whd_all env sigma t1) &&
         isSort sigma (whd_all env sigma t2)
       then (mayneedglobalcheck := true; sigma)
       else
         user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
-    else sigma
+    | Some sigma -> sigma
   end
   else
     if not (isSort sigma (whd_all env sigma t1)) then
@@ -815,9 +814,9 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
 let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
   let (sigma, t') = t sigma in
   let sigma = check_types env sigma mayneedglobalcheck deep t' c in
-  let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
-  if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
-  (sigma, t')
+  match infer_conv ~pb:cv_pb env sigma t' c with
+  | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
+  | Some sigma -> (sigma, t')
 
 (* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb deep t where env sigma c =
@@ -1934,16 +1933,19 @@ let assumption =
     let t = NamedDecl.get_type decl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
-    let (sigma, is_same_type) =
-      if only_eq then (sigma, EConstr.eq_constr sigma t concl)
+    let ans =
+      if only_eq then
+        if EConstr.eq_constr sigma t concl then Some sigma
+        else None
       else
         let env = Proofview.Goal.env gl in
         infer_conv env sigma t concl
     in
-    if is_same_type then
+    match ans with
+    | Some sigma ->
       (Proofview.Unsafe.tclEVARS sigma) <*>
 	exact_no_check (mkVar (NamedDecl.get_id decl))
-    else arec gl only_eq rest
+    | None -> arec gl only_eq rest
   in
   let assumption_tac gl =
     let hyps = Proofview.Goal.hyps gl in