search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.71k stars 637 forks source link

Ltac2 pattern matching fails to handle open terms #10115

Open JasonGross opened 6 years ago

JasonGross commented 6 years ago 
Require Ltac2.Ltac2.
Require Import Ltac2.Init Ltac2.Control Ltac2.Notations.
Goal (fun (x : nat) => let y := x in fun x : nat => y + x) = (fun x y : nat => x).
  cbv beta iota zeta.
  (*match goal with
  | [ |- (fun a b => ?C) = _ ]
    => idtac a b
  end.*)
  let g := Control.goal () in
  let matches := Pattern.matches pattern:((fun a b => _) = _) g in
  (). (* success *)
  let g := Control.goal () in
  let matches := Pattern.matches pattern:((fun a b => ?C) = _) g in
  (). (* failure *)
jfehrle commented 4 years ago

Needs a response. I presume the ?C case should also return "success".