Chasing a few unsafe constr coercions.

11 files changed, 65 insertions, 102 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 6380e3fc1..b30702d0d 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -941,37 +941,8 @@ let universes evd = UState.ugraph evd.universes
 let update_sigma_env evd env =
   { evd with universes = UState.update_sigma_env evd.universes env }
 
-(* Conversion w.r.t. an evar map and its local universes. *)
-
-let test_conversion_gen env evd pb t u =
-  match pb with 
-  | Reduction.CONV -> 
-    Reduction.conv env
-      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
-      t u
-  | Reduction.CUMUL -> Reduction.conv_leq env
-      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
-      t u
-
-let test_conversion env d pb t u =
-  try test_conversion_gen env d pb t u; true
-  with _ -> false
-
 exception UniversesDiffer = UState.UniversesDiffer
 
-let eq_constr_univs evd t u =
-  let fold cstr sigma =
-    try Some (add_universe_constraints sigma cstr)
-    with Univ.UniverseInconsistency _ | UniversesDiffer -> None
-  in
-  match Universes.eq_constr_univs_infer (UState.ugraph evd.universes) fold t u evd with
-  | None -> evd, false
-  | Some evd -> evd, true
-
-let e_eq_constr_univs evdref t u =
-  let evd, b = eq_constr_univs !evdref t u in
-    evdref := evd; b
-
 (**********************************************************)
 (* Side effects *)
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 699b52c2b..eeb9fd861 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -569,19 +569,6 @@ val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor ->
 val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
   evar_map -> Globnames.global_reference -> evar_map * constr
 
-(********************************************************************
-  Conversion w.r.t. an evar map, not unifying universes. See 
-  [Reductionops.infer_conv] for conversion up-to universes. *)
-
-val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
-(** WARNING: This does not allow unification of universes *)
-
-val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
-(** Syntactic equality up to universes, recording the associated constraints *)
-
-val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
-(** Syntactic equality up to universes. *)
-
 (********************************************************************)
 (* constr with holes and pending resolution of classes, conversion  *)
 (* problems, candidates, etc.                                       *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f5cab070e..1cbea68dd 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -973,7 +973,13 @@ let apply_on_subterm env evdref f c t =
     (* By using eq_constr, we make an approximation, for instance, we *)
     (* could also be interested in finding a term u convertible to t *)
     (* such that c occurs in u *)
-    if e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) then f k
+    let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with
+    | None -> false
+    | Some cstr ->
+      try ignore (Evd.add_universe_constraints !evdref cstr); true
+      with UniversesDiffer -> false
+    in
+    if eq_constr c t then f k
     else
       match EConstr.kind !evdref t with
       | Evar (evk,args) ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ff4736528..28e63d04b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1263,7 +1263,13 @@ type conv_fun_bool =
 
 let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
   let evdref = ref evd in
-  if Array.equal (fun c1 c2 -> e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) ) argsv1 argsv2 then !evdref else
+  let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with
+  | None -> false
+  | Some cstr ->
+    try ignore (Evd.add_universe_constraints !evdref cstr); true
+    with UniversesDiffer -> false
+  in
+  if Array.equal eq_constr argsv1 argsv2 then !evdref else
   (* Filter and restrict if needed *)
   let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
   let untypedfilter =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 4b027a127..97c5cda77 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -41,10 +41,8 @@ let project  = Refiner.project
 let pf_env   = Refiner.pf_env
 let pf_hyps  = Refiner.pf_hyps
 
-let test_conversion cb env sigma c1 c2 =
-  let c1 = EConstr.Unsafe.to_constr c1 in
-  let c2 = EConstr.Unsafe.to_constr c2 in
-  test_conversion cb env sigma c1 c2
+let test_conversion env sigma pb c1 c2 =
+  Reductionops.check_conv ~pb env sigma c1 c2
 
 let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
 let pf_hyps_types gls  =
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 491bc8b4a..b4a235ba8 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -8,6 +8,7 @@
 
 open Util
 open Term
+open EConstr
 open Names
 open Pattern
 open Globnames
@@ -38,18 +39,18 @@ let decomp_pat =
   in
   decrec []
 
-let decomp =
-  let rec decrec acc c = match kind_of_term c with
+let decomp sigma t =
+  let rec decrec acc c = match EConstr.kind sigma c with
     | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
     | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc)
     | Cast (c1,_,_) -> decrec acc c1
     | _ -> (c,acc)
   in
-    decrec []
+    decrec [] t
 
-let constr_val_discr t =
-  let c, l = decomp t in
-    match kind_of_term c with
+let constr_val_discr sigma t =
+  let c, l = decomp sigma t in
+    match EConstr.kind sigma c with
     | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
     | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
     | Var id -> Label(GRLabel (VarRef id),l)
@@ -66,9 +67,9 @@ let constr_pat_discr t =
     | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
     | _ -> None
 
-let constr_val_discr_st (idpred,cpred) t =
-  let c, l = decomp t in
-    match kind_of_term c with
+let constr_val_discr_st sigma (idpred,cpred) t =
+  let c, l = decomp sigma t in
+    match EConstr.kind sigma c with
     | Const (c,u) -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l)
     | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
     | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
@@ -105,11 +106,11 @@ let bounded_constr_pat_discr_st st (t,depth) =
       | None -> None
       | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 
-let bounded_constr_val_discr_st st (t,depth) =
+let bounded_constr_val_discr_st sigma st (t,depth) =
   if Int.equal depth 0 then
     Nothing
   else
-    match constr_val_discr_st st t with
+    match constr_val_discr_st sigma st t with
       | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
       | Nothing -> Nothing
       | Everything -> Everything
@@ -122,11 +123,11 @@ let bounded_constr_pat_discr (t,depth) =
       | None -> None
       | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 
-let bounded_constr_val_discr (t,depth) =
+let bounded_constr_val_discr sigma (t,depth) =
   if Int.equal depth 0 then
     Nothing
   else
-    match constr_val_discr t with
+    match constr_val_discr sigma t with
       | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
       | Nothing -> Nothing
       | Everything -> Everything
@@ -162,13 +163,13 @@ struct
 	(fun dn (c,v) ->
 	 Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
 
-  let lookup = function
+  let lookup sigma = function
     | None ->
 	(fun dn t ->
-	     Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))
+	     Dn.lookup dn (bounded_constr_val_discr sigma) (t,!dnet_depth))
     | Some st ->
 	(fun dn t ->
-	     Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth))
+	     Dn.lookup dn (bounded_constr_val_discr_st sigma st) (t,!dnet_depth))
 
   let app f dn = Dn.app f dn
 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 8ca5549b8..2a5e7c345 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -33,7 +33,7 @@ sig
   val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t
   val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t
 
-  val lookup : transparent_state option -> t -> constr -> Z.t list
+  val lookup : Evd.evar_map -> transparent_state option -> t -> EConstr.constr -> Z.t list
   val app : (Z.t -> unit) -> t -> unit
 end
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 122b64777..7f7a07b8f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1300,19 +1300,6 @@ let build_injector env sigma dflt c cpath =
   let sigma, (injcode,resty,_) = build_injrec env sigma dflt c cpath in
     sigma, (injcode,resty)
 
-(*
-let try_delta_expand env sigma t =
-  let whdt = whd_all env sigma t  in
-  let rec hd_rec c  =
-    match kind_of_term c with
-      | Construct _ -> whdt
-      | App (f,_)  -> hd_rec f
-      | Cast (c,_,_) -> hd_rec c
-      | _  -> t
-  in
-  hd_rec whdt
-*)
-
 let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
 let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ffd19ac6e..17c81064d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -250,9 +250,8 @@ let rebuild_dn st se =
   in
   { se with sentry_bnet = dn' }
 
-let lookup_tacs concl st se =
-  let concl = EConstr.Unsafe.to_constr concl in
-  let l'  = Bounded_net.lookup st se.sentry_bnet concl in
+let lookup_tacs sigma concl st se =
+  let l'  = Bounded_net.lookup sigma st se.sentry_bnet concl in
   let sl' = List.stable_sort pri_order_int l' in
   List.merge pri_order_int se.sentry_nopat sl'
 
@@ -510,6 +509,17 @@ struct
       (** Warn about no longer typable hint? *)
       None
 
+  let head_evar sigma c =
+    let rec hrec c = match EConstr.kind sigma c with
+      | Evar (evk,_)   -> evk
+      | Case (_,_,c,_) -> hrec c
+      | App (c,_)      -> hrec c
+      | Cast (c,_,_)   -> hrec c
+      | Proj (p, c)    -> hrec c
+      | _              -> raise Evarutil.NoHeadEvar
+    in
+    hrec c
+
   let match_mode sigma m arg =
     match m with
     | ModeInput -> not (occur_existential sigma arg)
@@ -543,7 +553,7 @@ struct
   let map_auto sigma ~secvars (k,args) concl db =
     let se = find k db in
     let st = if db.use_dn then  (Some db.hintdb_state) else None in
-    let pat = lookup_tacs concl st se in
+    let pat = lookup_tacs sigma concl st se in
     merge_entry secvars db [] pat
 
   let map_existential sigma ~secvars (k,args) concl db =
@@ -557,7 +567,7 @@ struct
     let se = find k db in
       if matches_modes sigma args se.sentry_mode then
         let st = if db.use_dn then Some db.hintdb_state else None in
-        let pat = lookup_tacs concl st se in
+        let pat = lookup_tacs sigma concl st se in
         merge_entry secvars db [] pat
       else merge_entry secvars db [] []
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index de3572155..a29803251 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4831,8 +4831,11 @@ let intros_transitivity  n  = Tacticals.New.tclTHEN intros (transitivity_gen n)
 (** d1 is the section variable in the global context, d2 in the goal context *)
 let interpretable_as_section_decl evd d1 d2 =
   let open Context.Named.Declaration in
-  let e_eq_constr_univs sigma c1 c2 =
-    e_eq_constr_univs sigma (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2)
+  let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes !sigma c1 c2 with
+  | None -> false
+  | Some cstr ->
+    try ignore (Evd.add_universe_constraints !sigma cstr); true
+    with UniversesDiffer -> false
   in
   match d2, d1 with
   | LocalDef _, LocalAssum _ -> false
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b689dfcf9..50301ee0d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -83,8 +83,6 @@ let rec contract3' env sigma a b c = function
 
 (** Ad-hoc reductions *)
 
-let to_unsafe_judgment j = on_judgment EConstr.Unsafe.to_constr j
-
 let j_nf_betaiotaevar sigma j =
   { uj_val = Evarutil.nf_evar sigma j.uj_val;
     uj_type = Reductionops.nf_betaiota sigma j.uj_type }
@@ -207,7 +205,7 @@ let pr_puniverses f env (c,u) =
   else mt())
 
 let explain_elim_arity env sigma ind sorts c pj okinds =
-  let pj = to_unsafe_judgment pj in
+  let open EConstr in
   let env = make_all_name_different env in
   let pi = pr_inductive env (fst ind) in
   let pc = pr_leconstr_env env sigma c in
@@ -223,7 +221,7 @@ let explain_elim_arity env sigma ind sorts c pj okinds =
 	| WrongArity ->
 	  "wrong arity" in
       let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in
-      let ppt = pr_lconstr_env env sigma ((strip_prod_assum pj.uj_type)) in
+      let ppt = pr_leconstr_env env sigma (snd (decompose_prod_assum sigma pj.uj_type)) in
       hov 0
 	(str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
 	 str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++
@@ -243,11 +241,10 @@ let explain_elim_arity env sigma ind sorts c pj okinds =
 
 let explain_case_not_inductive env sigma cj =
   let cj = Evarutil.j_nf_evar sigma cj in
-  let cj = to_unsafe_judgment cj in
   let env = make_all_name_different env in
-  let pc = pr_lconstr_env env sigma cj.uj_val in
-  let pct = pr_lconstr_env env sigma cj.uj_type in
-    match kind_of_term cj.uj_type with
+  let pc = pr_leconstr_env env sigma cj.uj_val in
+  let pct = pr_leconstr_env env sigma cj.uj_type in
+    match EConstr.kind sigma cj.uj_type with
       | Evar _ ->
 	  str "Cannot infer a type for this expression."
       | _ ->
@@ -257,10 +254,9 @@ let explain_case_not_inductive env sigma cj =
 
 let explain_number_branches env sigma cj expn =
   let cj = Evarutil.j_nf_evar sigma cj in
-  let cj = to_unsafe_judgment cj in
   let env = make_all_name_different env in
-  let pc = pr_lconstr_env env sigma cj.uj_val in
-  let pct = pr_lconstr_env env sigma cj.uj_type in
+  let pc = pr_leconstr_env env sigma cj.uj_val in
+  let pct = pr_leconstr_env env sigma cj.uj_type in
   str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++
   str "of type" ++ brk(1,1) ++ pct ++ spc () ++
   str "expects " ++  int expn ++ str " branches."
@@ -390,18 +386,16 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
 
 let explain_cant_apply_not_functional env sigma rator randl =
   let randl = Evarutil.jv_nf_evar sigma randl in
-  let randl = Array.map to_unsafe_judgment randl in
   let rator = Evarutil.j_nf_evar sigma rator in
-  let rator = to_unsafe_judgment rator in
   let env = make_all_name_different env in
   let nargs = Array.length randl in
 (*  let pe = pr_ne_context_of (str "in environment") env sigma in*)
-  let pr = pr_lconstr_env env sigma rator.uj_val in
-  let prt = pr_lconstr_env env sigma rator.uj_type in
+  let pr = pr_leconstr_env env sigma rator.uj_val in
+  let prt = pr_leconstr_env env sigma rator.uj_type in
   let appl = prvect_with_sep fnl
 	       (fun c ->
-		  let pc = pr_lconstr_env env sigma c.uj_val in
-		  let pct = pr_lconstr_env env sigma c.uj_type in
+		  let pc = pr_leconstr_env env sigma c.uj_val in
+		  let pct = pr_leconstr_env env sigma c.uj_type in
 		  hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
   in
   str "Illegal application (Non-functional construction): " ++