diff options
| author | Pierre-Marie Pédrot | 2020-12-26 16:16:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-12 18:52:07 +0100 |
| commit | d006c50c55e4ac3fcf9dcc972b07cbf3961f143c (patch) | |
| tree | e16c5e1cf407e6d577ac486a87bb3a6e179da386 /pretyping | |
| parent | 14a56d4aa1c92c66398b8e3d49d47e2d40748c48 (diff) | |
Same treatment for pattern functions used by rewrite.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 6 |
1 files 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) -> |