Merge pull request #47 from SkySkimmer/no-hresolve

Adapt to coq/coq#17035 (remove hresolve)
snu-sf · Dec 29, 2022 · ec2dd14 · ec2dd14
2 parents 4f140d2 + d31a48b
commit ec2dd14
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 113 deletions.
diff --git a/metasrc/pacotac_internal.py b/metasrc/pacotac_internal.py
@@ -8,7 +8,6 @@
 
 relsize = int(sys.argv[1])
 
-print ('From Paco Require Import hpattern.')
 print ('From Paco Require Export paconotation_internal paconotation.')
 print ('Set Implicit Arguments.')
 print ()
@@ -24,6 +23,8 @@
 print ()
 print ('(** ** Internal tactics *)')
 print ()
+print ('Ltac get_concl := lazymatch goal with [ |- ?G ] => G end.')
+print ()
 print ('Inductive _paco_mark := _paco_mark_cons.')
 print ()
 print ('Inductive _paco_foo := _paco_foo_cons.')

diff --git a/src/hpattern.v b/src/hpattern.v
diff --git a/src/pacotac_internal.v b/src/pacotac_internal.v
@@ -1,4 +1,3 @@
-From Paco Require Import hpattern.
 From Paco Require Export paconotation_internal paconotation.
 Set Implicit Arguments.
 
@@ -14,6 +13,8 @@ Set Implicit Arguments.
 
 (** ** Internal tactics *)
 
+Ltac get_concl := lazymatch goal with [ |- ?G ] => G end.
+
 Inductive _paco_mark := _paco_mark_cons.
 
 Inductive _paco_foo := _paco_foo_cons.