From d006c50c55e4ac3fcf9dcc972b07cbf3961f143c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Dec 2020 16:16:18 +0100
Subject: Same treatment for pattern functions used by rewrite.

---
 pretyping/unification.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2bd49ba47d..83e46e3295 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1779,6 +1779,7 @@ let keyed_unify env evd kop =
 let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
   let bestexn = ref None in
   let kop = Keys.constr_key (fun c -> EConstr.kind evd c) op in
+  let opgnd = if occur_meta_or_undefined_evar evd op then NotGround else Ground in
   let rec matchrec cl =
     let cl = strip_outer_cast evd cl in
     (try
@@ -1788,7 +1789,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
            let f1, l1 = decompose_app_vect evd op in
            let f2, l2 = decompose_app_vect evd cl in
            w_typed_unify_array env evd flags f1 l1 f2 l2,cl
-         else w_typed_unify env evd CONV flags (op, Unknown) (cl, Unknown),cl
+         else w_typed_unify env evd CONV flags (op, opgnd) (cl, Unknown),cl
        with ex when Pretype_errors.unsatisfiable_exception ex ->
             bestexn := Some ex; user_err Pp.(str "Unsat"))
        else user_err Pp.(str "Bound 1")
@@ -1883,11 +1884,12 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
       else bind (f a.(i)) (ffail (i+1))
     in ffail 0
   in
+  let opgnd = if occur_meta_or_undefined_evar evd op then NotGround else Ground in
   let rec matchrec cl =
     let cl = strip_outer_cast evd cl in
       (bind
           (if closed0 evd cl
-          then return (fun () -> w_typed_unify env evd CONV flags (op, Unknown) (cl, Unknown),cl)
+          then return (fun () -> w_typed_unify env evd CONV flags (op, opgnd) (cl, Unknown),cl)
             else fail "Bound 1")
           (match EConstr.kind evd cl with
             | App (f,args) ->
-- 
cgit v1.2.3