Chasing a few unsafe constr coercions.

5 files changed, 38 insertions, 37 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 491bc8b4ab..b4a235ba8c 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 8ca5549b88..2a5e7c3458 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 122b64777e..7f7a07b8fe 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 ffd19ac6e0..17c81064d7 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 de35721555..a29803251e 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