Rename types_or_terms and the unification function types

1 files changed, 33 insertions, 27 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aad21ad932..2ff52d1657 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -33,6 +33,34 @@ type unify_flags = {
   allow_K_at_toplevel : bool;
   with_cs : bool }
 
+type unification_kind =
+  | TypeUnification
+  | TermUnification
+
+(************************)
+(* Unification results  *)
+(************************)
+
+type unification_result =
+  | Success of evar_map
+  | UnifFailure of evar_map * unification_error
+
+let is_success = function Success _ -> true | UnifFailure _ -> false
+
+let test_success conv_algo b env evd c c' rhs =
+  is_success (conv_algo b env evd c c' rhs)
+
+(** A unification function: parameterized by the kind of unification,
+    environment, sigma, conversion problem and the two terms to unify. *)
+type unifier = unification_kind ->
+  env -> evar_map -> conv_pb -> constr -> constr -> unification_result
+
+(** A conversion function: parameterized by the kind of unification,
+    environment, sigma, conversion problem and the two terms to convert.
+    Conversion is not allowed to instantiate evars contrary to unification. *)
+type conversion_check = unification_kind ->
+  env ->  evar_map -> conv_pb -> constr -> constr -> bool
+
 let normalize_evar evd ev =
   match EConstr.kind evd (mkEvar ev) with
   | Evar (evk,args) -> (evk,args)
@@ -138,20 +166,6 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
   let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
     refresh_universes (Some false) env sigma ty
-		      
-
-(************************)
-(* Unification results  *)
-(************************)
-
-type unification_result =
-  | Success of evar_map
-  | UnifFailure of evar_map * unification_error
-
-let is_success = function Success _ -> true | UnifFailure _ -> false
-
-let test_success conv_algo b env evd c c' rhs =
-  is_success (conv_algo b env evd c c' rhs)
 
 let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
   match pbty with
@@ -174,7 +188,7 @@ let recheck_applications conv_algo env evdref t =
 	 if i < Array.length argsty then
 	 match EConstr.kind !evdref (whd_all env !evdref ty) with
 	 | Prod (na, dom, codom) ->
-            (match conv_algo true env !evdref Reduction.CUMUL argsty.(i) dom with
+            (match conv_algo TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
 			     aux (succ i) (subst1 args.(i) codom)
 	     | UnifFailure (evd, reason) ->
@@ -752,7 +766,7 @@ let check_evar_instance evd evk1 body conv_algo =
     try Retyping.get_type_of ~lax:true evenv evd body
     with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance"))
   in
-  match conv_algo true evenv evd Reduction.CUMUL ty evi.evar_concl with
+  match conv_algo TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
@@ -1135,7 +1149,7 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
 
 let filter_compatible_candidates conv_algo env evd evi args rhs c =
   let c' = instantiate_evar_array evi c args in
-  match conv_algo false env evd Reduction.CONV rhs c' with
+  match conv_algo TermUnification env evd Reduction.CONV rhs c' with
   | Success evd -> Some (c,evd)
   | UnifFailure _ -> None
 
@@ -1331,14 +1345,6 @@ let solve_evar_evar ?(force=false) flags f g env evd pbty (evk1,args1 as ev1) (e
       evd in
   solve_evar_evar_aux force flags f g env evd pbty ev1 ev2
 
-type types_or_terms = bool
-
-type conv_fun =
-  types_or_terms -> env ->  evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> unification_result
-
-type conv_fun_bool =
-  types_or_terms -> env ->  evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> bool
-
 (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
  * definitions. We try to unify the ti with the ui pairwise. The pairs
  * that don't unify are discarded (i.e. ?e is redefined so that it does not
@@ -1357,7 +1363,7 @@ let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2
   let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
   let untypedfilter =
     restrict_upon_filter evd evk
-      (fun (a1,a2) -> conv_algo false env evd Reduction.CONV a1 a2) args in
+      (fun (a1,a2) -> conv_algo TermUnification env evd Reduction.CONV a1 a2) args in
   let candidates = filter_candidates evd evk untypedfilter NoUpdate in
   let filter = closure_of_filter evd evk untypedfilter in
   let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
@@ -1696,7 +1702,7 @@ let reconsider_unif_constraints conv_algo evd =
     (fun p (pbty,env,t1,t2 as x) ->
        match p with
        | Success evd ->
-           (match conv_algo true env evd pbty t1 t2 with
+           (match conv_algo TermUnification env evd pbty t1 t2 with
            | Success _ as x -> x
            | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e)))
        | UnifFailure _ as x -> x)