Deprecate Evarconv.e_conv,e_cumul

6 files changed, 95 insertions, 61 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 16244d8c0..84f0aba8c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -315,13 +315,15 @@ let try_find_ind env sigma typ realnames =
   IsInd (typ,ind,names)
 
 let inh_coerce_to_ind evdref env loc ty tyi =
-  let sigma = !evdref in
+  let orig = !evdref in
   let expected_typ = inductive_template evdref env loc tyi in
   (* Try to refine the type with inductive information coming from the
      constructor and renounce if not able to give more information *)
   (* devrait être indifférent d'exiger leq ou pas puisque pour
      un inductif cela doit être égal *)
-  if not (e_cumul env evdref expected_typ ty) then evdref := sigma
+  match cumul env !evdref expected_typ ty with
+  | Some sigma -> evdref := sigma
+  | None -> evdref := orig
 
 let binding_vars_of_inductive sigma = function
   | NotInd _ -> []
@@ -427,7 +429,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 	    let current =
 	      if List.is_empty deps && isEvar !(pb.evdref) typ then
 	      (* Don't insert coercions if dependent; only solve evars *)
-		let _ = e_cumul pb.env pb.evdref indt typ in
+                let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in
 		current
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to true pb.env)
@@ -1738,9 +1740,10 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
         let evd,tt = Typing.type_of extenv !evdref t in
         evdref := evd;
         (t,tt) in
-  let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
-  if not b then anomaly (Pp.str "Build_tycon: should be a type.");
-  { uj_val = t; uj_type = tt }
+  match cumul env !evdref tt (mkSort s) with
+  | None -> anomaly (Pp.str "Build_tycon: should be a type.");
+  | Some sigma -> evdref := sigma;
+    { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
  * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e8b17d694..ea8557b18 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -48,31 +48,35 @@ exception NoCoercion
 exception NoCoercionNoUnifier of evar_map * unification_error
 
 (* Here, funj is a coercion therefore already typed in global context *)
-let apply_coercion_args env evd check isproj argl funj =
-  let evdref = ref evd in
-  let rec apply_rec acc typ = function
+let apply_coercion_args env sigma check isproj argl funj =
+  let rec apply_rec sigma acc typ = function
     | [] ->
       if isproj then
-	let cst = fst (destConst !evdref (j_val funj)) in
+        let cst = fst (destConst sigma (j_val funj)) in
 	let p = Projection.make cst false in
 	let pb = lookup_projection p env in
 	let args = List.skipn pb.Declarations.proj_npars argl in
 	let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
-	  { uj_val = applist (mkProj (p, hd), tl);
-	    uj_type = typ }
+        sigma, { uj_val = applist (mkProj (p, hd), tl);
+                 uj_type = typ }
       else
-	{ uj_val = applist (j_val funj,argl);
-	  uj_type = typ }
+        sigma, { uj_val = applist (j_val funj,argl);
+                 uj_type = typ }
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
-      match EConstr.kind !evdref (whd_all env !evdref typ) with
+      match EConstr.kind sigma (whd_all env sigma typ) with
       | Prod (_,c1,c2) ->
-        if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then
-	  raise NoCoercion;
-        apply_rec (h::acc) (subst1 h c2) restl
+        let sigma =
+          if check then
+            begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with
+              | None -> raise NoCoercion
+              | Some sigma -> sigma
+            end
+          else sigma
+        in
+        apply_rec sigma (h::acc) (subst1 h c2) restl
       | _ -> anomaly (Pp.str "apply_coercion_args.")
   in
-  let res = apply_rec [] funj.uj_type argl in
-    !evdref, res
+  apply_rec sigma [] funj.uj_type argl
 
 (* appliquer le chemin de coercions de patterns p *)
 let apply_pattern_coercion ?loc pat p =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index da2b4d1b8..bea3eeb2e 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -28,7 +28,10 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma
 (** The same function resolving evars by side-effect and
    catching the exception *)
 val e_conv  : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
+[@@ocaml.deprecated "Use [Evarconv.conv]"]
+
 val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
+[@@ocaml.deprecated "Use [Evarconv.cumul]"]
 
 val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
 val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e68a25a87..35cc5702a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -674,14 +674,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
     let nbfix = Array.length lar in
     let names = Array.map (fun id -> Name id) names in
-    let _ = 
+    let () =
       match tycon with
       | Some t -> 
  	let fixi = match fixkind with
 	  | GFix (vn,i) -> i
 	  | GCoFix i -> i
-	in e_conv env.ExtraEnv.env evdref ftys.(fixi) t
-      | None -> true
+        in
+        begin match conv env.ExtraEnv.env !evdref ftys.(fixi) t with
+          | None -> ()
+          | Some sigma -> evdref := sigma
+        end
+      | None -> ()
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
     let newenv = push_rec_types !evdref (names,ftys,[||]) env in
@@ -698,7 +702,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         ctxtv vdef in
-      Typing.check_type_fixpoint ?loc env.ExtraEnv.env evdref names ftys vdefj;
+      evdref := Typing.check_type_fixpoint ?loc env.ExtraEnv.env !evdref names ftys vdefj;
       let nf c = nf_evar !evdref c in
       let ftys = Array.map nf ftys in (** FIXME *)
       let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in
@@ -793,9 +797,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      match candargs with
 	      | [] -> [], j_val hj
 	      | arg :: args -> 
-		if e_conv env.ExtraEnv.env evdref (j_val hj) arg then
-		  args, nf_evar !evdref (j_val hj)
-		else [], j_val hj
+                begin match conv env.ExtraEnv.env !evdref (j_val hj) arg with
+                  | Some sigma -> evdref := sigma;
+                    args, nf_evar !evdref (j_val hj)
+                  | None ->
+                    [], j_val hj
+                end
 	    in
             let ujval = adjust_evar_source evdref na ujval in
 	    let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
@@ -1166,10 +1173,12 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
 	match valcon with
 	| None -> tj
 	| Some v ->
-	    if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
-	    else
+          begin match cumul env.ExtraEnv.env !evdref v tj.utj_val with
+            | Some sigma -> evdref := sigma; tj
+            | None ->
 	      error_unexpected_type
                 ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
+          end
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let env = make_env env sigma in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index aaec73f04..da72d7a75 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -69,10 +69,12 @@ let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv =
          | _ ->
              error_cant_apply_not_functional env !evdref funj argjv
        in
-       if Evarconv.e_cumul env evdref hj.uj_type c1 then
-         apply_rec (n+1) (subst1 hj.uj_val c2) restjl
-       else
-         error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+       begin match Evarconv.cumul env !evdref hj.uj_type c1 with
+         | Some sigma -> evdref := sigma;
+           apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+         | None ->
+           error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+       end
   in
   apply_rec 1 funj.uj_type (Array.to_list argjv)
 
@@ -93,20 +95,24 @@ let e_judge_of_apply env evdref funj argjv =
          | _ ->
             error_cant_apply_not_functional env !evdref funj argjv
        in
-       if Evarconv.e_cumul env evdref hj.uj_type c1 then
-         apply_rec (n+1) (subst1 hj.uj_val c2) restjl
-       else
-         error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+       begin match Evarconv.cumul env !evdref hj.uj_type c1 with
+         | Some sigma -> evdref := sigma;
+           apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+         | None ->
+           error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+       end
   in
   apply_rec 1 funj.uj_type (Array.to_list argjv)
 
-let e_check_branch_types env evdref (ind,u) cj (lfj,explft) =
+let check_branch_types env sigma (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
-    error_number_branches env !evdref cj (Array.length explft);
-  for i = 0 to Array.length explft - 1 do
-    if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then
-      error_ill_formed_branch env !evdref cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
-  done
+    error_number_branches env sigma cj (Array.length explft);
+  Array.fold_left2_i (fun i sigma lfj explft ->
+      match Evarconv.cumul env sigma lfj.uj_type explft with
+      | Some sigma -> sigma
+      | None ->
+        error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft)
+    sigma lfj explft
 
 let max_sort l =
   if Sorts.List.mem InType l then InType else
@@ -120,8 +126,11 @@ let e_is_correct_arity env evdref c pj ind specif params =
     let pt' = whd_all env !evdref pt in
     match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-        if not (Evarconv.e_cumul env evdref a1 a1') then error ();
-        srec (push_rel (LocalAssum (na1,a1)) env) t ar'
+      begin match Evarconv.cumul env !evdref a1 a1' with
+        | None -> error ()
+        | Some sigma -> evdref := sigma;
+          srec (push_rel (LocalAssum (na1,a1)) env) t ar'
+      end
     | Sort s, [] ->
         let s = ESorts.kind !evdref s in
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
@@ -167,19 +176,21 @@ let e_judge_of_case env evdref ci pj cj lfj =
   let indspec = ((ind, EInstance.kind !evdref u), spec) in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
-  e_check_branch_types env evdref (fst indspec) cj (lfj,bty);
+  evdref := check_branch_types env !evdref (fst indspec) cj (lfj,bty);
   { uj_val  = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
     uj_type = rslty }
 
-let check_type_fixpoint ?loc env evdref lna lar vdefj =
+let check_type_fixpoint ?loc env sigma lna lar vdefj =
   let lt = Array.length vdefj in
-    if Int.equal (Array.length lar) lt then
-      for i = 0 to lt-1 do
-        if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
-		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body ?loc env !evdref
-            i lna vdefj lar
-      done
+  assert (Int.equal (Array.length lar) lt);
+  Array.fold_left2_i (fun i sigma defj ar ->
+      match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with
+      | Some sigma -> sigma
+      | None ->
+        error_ill_typed_rec_body ?loc env sigma
+          i lna vdefj lar)
+    sigma vdefj lar
+
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
@@ -194,10 +205,12 @@ let check_allowed_sort env sigma ind c p =
 
 let e_judge_of_cast env evdref cj k tj =
   let expected_type = tj.utj_val in
-  if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
+  match Evarconv.cumul env !evdref cj.uj_type expected_type with
+  | None ->
     error_actual_type_core env !evdref cj expected_type;
-  { uj_val = mkCast (cj.uj_val, k, expected_type);
-    uj_type = expected_type }
+  | Some sigma -> evdref := sigma;
+    { uj_val = mkCast (cj.uj_val, k, expected_type);
+      uj_type = expected_type }
 
 let enrich_env env evdref =
   let penv = Environ.pre_env env in
@@ -374,7 +387,7 @@ and execute_recdef env evdref (names,lar,vdef) =
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
   let vdefv = Array.map j_val vdefj in
-  let _ = check_type_fixpoint env1 evdref names lara vdefj in
+  evdref := check_type_fixpoint env1 !evdref names lara vdefj;
   (names,lara,vdefv)
 
 and execute_array env evdref = Array.map (execute env evdref)
@@ -382,8 +395,10 @@ and execute_array env evdref = Array.map (execute env evdref)
 let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-  if not (Evarconv.e_cumul env evdref j.uj_type t) then
+  match Evarconv.cumul env !evdref j.uj_type t with
+  | None ->
     error_actual_type_core env !evdref j t
+  | Some sigma -> evdref := sigma
 
 (* Type of a constr *)
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 4905adf1f..2239dda5f 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -46,8 +46,8 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
 
 (** Raise an error message if bodies have types not unifiable with the
     expected ones *)
-val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ref ->
-  Names.Name.t array -> types array -> unsafe_judgment array -> unit
+val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ->
+  Names.Name.t array -> types array -> unsafe_judgment array -> evar_map
 
 val judge_of_prop : unsafe_judgment
 val judge_of_set : unsafe_judgment