Merge PR coq#9826: [ssr] Two small improvements

Reviewed-by: gares

plugins/ssr/ssrequality.ml

@@ -325,7 +325,7 @@ let rec strip_prod_assum c = match Constr.kind c with
 
 let rule_id = mk_internal_id "rewrite rule"
 
-exception PRtype_error
+exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option
 
 let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
 (*   ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *)
@@ -351,7 +351,10 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
   let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
   (* We check the proof is well typed *)
   let sigma, proof_ty =
-    try Typing.type_of env sigma proof with _ -> raise PRtype_error in
+    try Typing.type_of env sigma proof with
+    | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te)))
+    | e when CErrors.noncritical e -> raise (PRtype_error None)
+  in
   ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
   try refine_with 
     ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl
@@ -423,13 +426,17 @@ let rwcltac cl rdx dir sr gl =
   in
   let cvtac' _ =
     try cvtac gl with
-    | PRtype_error ->
+    | PRtype_error e ->
+      let error = Option.cata (fun (env, sigma, te) ->
+          Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te))
+          (Pp.mt ()) e in
       if occur_existential (project gl) (Tacmach.pf_concl gl)
-      then errorstrm Pp.(str "Rewriting impacts evars")
+      then errorstrm Pp.(str "Rewriting impacts evars" ++ error)
       else errorstrm Pp.(str "Dependent type error in rewrite of "
         ++ pr_constr_env (pf_env gl) (project gl)
           (Term.mkNamedLambda (make_annot pattern_id Sorts.Relevant)
-             (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl)))
+             (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))
+        ++ error)
   in
   tclTHEN cvtac' rwtac gl
 

plugins/ssr/ssripats.ml

@@ -369,18 +369,20 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl ->
 end end
 
 (*** [=> [: id]] ************************************************************)
-[@@@ocaml.warning "-3"]
 let mk_abstract_id =
   let open Coqlib in
   let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in
-begin fun () ->
+begin fun env sigma ->
+  let sigma, zero = EConstr.fresh_global env sigma (lib_ref "num.nat.O") in
+  let sigma, succ = EConstr.fresh_global env sigma (lib_ref "num.nat.S") in
   let rec nat_of_n n =
-    if n = 0 then EConstr.mkConstruct path_of_O
-    else EConstr.mkApp (EConstr.mkConstruct path_of_S, [|nat_of_n (n-1)|]) in
-  incr ssr_abstract_id; nat_of_n !ssr_abstract_id
+    if n = 0 then zero
+    else EConstr.mkApp (succ, [|nat_of_n (n-1)|]) in
+  incr ssr_abstract_id;
+  sigma, nat_of_n !ssr_abstract_id
 end
 
-let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
+let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
   let env, concl = Goal.(env gl, concl gl) in
   let step = begin fun sigma ->
     let (sigma, (abstract_proof, abstract_ty)) =
@@ -389,8 +391,8 @@ let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
       let (sigma, ablock) = Ssrcommon.mkSsrConst "abstract_lock" env sigma in
       let (sigma, lock) = Evarutil.new_evar env sigma ablock in
       let (sigma, abstract) = Ssrcommon.mkSsrConst "abstract" env sigma in
-      let abstract_ty =
-        EConstr.mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in
+      let (sigma, abstract_id) = mk_abstract_id env sigma in
+      let abstract_ty = EConstr.mkApp(abstract, [|ty; abstract_id; lock|]) in
       let sigma, m = Evarutil.new_evar env sigma abstract_ty in
       sigma, (m, abstract_ty) in
     let sigma, kont =
@@ -409,7 +411,7 @@ end
 
 let tclMK_ABSTRACT_VARS ids =
   List.fold_right (fun id tac ->
-    Tacticals.New.tclTHENFIRST (tcltclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ())
+    Tacticals.New.tclTHENFIRST (tclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ())
 
 (* Debugging *)
 let tclLOG p t =