Add the #[export] attribute

theories/cancelCTC.v

@@ -34,6 +34,7 @@ Arguments Ast : clear implicits.
 
 
 (* pass output context of f1 as input of f2 *)
+#[export]
 Program Instance
   union_struct i j k t1 t2 h1 h2 (f1 : Ast i j t1 h1) (f2 : Ast j k t2 h2) :
   Ast i k (t1 ++ t2) (h1 :+ h2) | 3.
@@ -44,12 +45,14 @@ split; first by rewrite interp_cat (interp_subctx D1 S2).
 by rewrite valid_cat D2 andbT; apply: (valid_subctx S2).
 Qed.
 
+#[export]
 Program Instance empty_struct i :
   Ast i i [::] empty | 1.
 Next Obligation.
 split; by [|apply: subctx_refl|].
 Qed.
 
+#[export]
 Program Instance
   pts_struct A hs xs1 x (d : A)
            (f : XFind xs1 x) :
@@ -62,7 +65,7 @@ case: f=>[xs2 n /= [H P]]; split; first by rewrite /= H.
 by apply/andP; rewrite /= (onth_size H).
 Qed.
 
-
+#[export]
 Program Instance var_struct hs1 xs h (f : XFind hs1 h) :
   Ast (Context hs1 xs) (Context seq_of xs) [:: Var index_of] h | 1000.
 Next Obligation.

theories/domains.v

@@ -99,6 +99,7 @@ Proof. by case: T y x z=>S [[l b B R A Tr]] ? x y z; apply: (Tr). Qed.
 
 End Laws.
 
+#[export]
 Hint Resolve botP poset_refl : core.
 
 Add Parametric Relation (T : poset) : T (@Poset.leq T)

theories/heaps.v

@@ -299,6 +299,7 @@ Qed.
 Lemma def0 : def empty.
 Proof. by []. Qed.
 
+#[export]
 Hint Resolve def0 : core.
 
 Lemma defU h x d : def (upd h x d) = (x != null) && (def h).
@@ -633,6 +634,7 @@ Proof. by rewrite -lt0n addn1. Qed.
 
 Opaque fresh.
 
+#[export]
 Hint Resolve dom_fresh fresh_null : core.
 
 (********)
@@ -744,6 +746,7 @@ apply/subdomP=>[//||x in1]; first by apply negbT.
 by apply: (subdomQ H2) (subdomQ H1 in1).
 Qed.
 
+#[export]
 Hint Resolve subdom_emp subdomPE : core.
 
 (***********)
@@ -1177,6 +1180,7 @@ Notation "h1 =~ h2" := (loweq h1 h2) (at level 80).
 Lemma low_refl h : h =~ h.
 Proof. by rewrite /loweq. Qed.
 
+#[export]
 Hint Resolve low_refl : core.
 
 Lemma low_sym h1 h2 : (h1 =~ h2) = (h2 =~ h1).
@@ -1223,6 +1227,7 @@ Qed.
 Lemma lowPn A1 A2 (x : ptr) (v1 : A1) (v2 : A2) : x :-> v1 =~ x :-> v2.
 Proof. by apply/loweqP=>y; rewrite !ldomP !domPt. Qed.
 
+#[export]
 Hint Resolve lowPn : core.
 
 Lemma highPn A1 A2 (x1 x2 : ptr) (v1 : A1) (v2 : A2) :

theories/indomCTC.v

@@ -27,19 +27,22 @@ Class Indom (x : ptr) (h : heap) :=
 
 Obligation Tactic := idtac.
 
+#[export]
 Program Instance found : forall A x (v : A), Indom x (x:->v).
 Next Obligation.
 move=> A x v; rewrite defPt => xnull.
 by rewrite domPt !inE eq_refl xnull.
 Qed.
 
+#[export]
 Program Instance found_left :
   forall x h1 h2 (xh1 : Indom x h1), Indom x (h1:+h2).
 Next Obligation.
 move=> x h1 h2 xh1 defh12; rewrite domUn !inE defh12.
 case: xh1 => xh1; by rewrite (xh1 (defUnl defh12)).
 Qed.
 
+#[export]
 Program Instance found_right :
   forall x h1 h2 (xh2 : Indom x h2), Indom x (h1:+h2).
 Next Obligation.

theories/noaliasCTC.v

@@ -33,6 +33,7 @@ Class Scan (h : heap) :=
         { seq_of : seq ptr ;
           scan : scan_axiom h seq_of }.
 
+#[export]
 Program Instance scan_union h1 h2 (f1 : Scan h1) (f2 : Scan h2) :
                    Scan (h1:+h2) | 2 := {| seq_of := @seq_of _ f1 ++ @seq_of _ f2 |}.
 Next Obligation.
@@ -46,12 +47,14 @@ apply/allP=>x; move/H2=>H3; apply: (introN idP); move/H1=>H4.
 by case: defUn D=>// _ _; move/(_ _ H4); rewrite H3.
 Qed.
 
+#[export]
 Program Instance scan_ptr A x (v : A) : Scan (x:->v) | 1 := {| seq_of :=  [:: x] |}.
 Next Obligation.
 rewrite /scan_axiom /= defPt => D; split=>//.
 by move=>y; rewrite inE; move/eqP=>->; rewrite domPt inE /= eq_refl D.
 Qed.
 
+#[export]
 Program Instance scan_default h : Scan h | 10 := {| seq_of := [::] |}.
 Next Obligation.
 by move=>_; split.
@@ -73,11 +76,13 @@ Abort.
 Class Search (x : ptr) (s : seq ptr) :=
         { search : x \in s }.
 
+#[export]
 Program Instance search_found x s : Search x (x :: s).
 Next Obligation.
 by rewrite inE eq_refl.
 Qed.
 
+#[export]
 Program Instance search_recurse x y s (f : Search x s) : Search x (y :: s) | 5.
 Next Obligation.
 by case: f; rewrite inE=>->; rewrite orbT.
@@ -95,18 +100,21 @@ Definition search2_axiom (x y : ptr) (s : seq ptr) :=
 
 Class Search2 x y s := { search2 : search2_axiom x y s}.
 
+#[export]
 Program Instance search2_foundx x y s (s1 : Search y s) : Search2 x y (x :: s).
 Next Obligation.
 case: s1=>s2; rewrite /search2_axiom !inE eq_refl.
 by rewrite s2 orbT; split=>//; case/andP=>H2 _; case: eqP s2 H2=>// -> ->.
 Qed.
 
+#[export]
 Program Instance search2_foundy x y s (f : Search x s) : Search2 x y (y :: s).
 Next Obligation.
 case: f=>H1; rewrite /search2_axiom !inE eq_refl.
 by rewrite H1 orbT; split=>//; case/andP=>H2 _; case: eqP H1 H2=>// -> ->.
 Qed.
 
+#[export]
 Program Instance search2_foundz x y z s (f : Search2 x y s) : Search2 x y (z :: s) | 1.
 Next Obligation.
 case: f=>[[H1 H2 H3]].
@@ -134,6 +142,7 @@ Qed.
 
 Arguments noaliasR [h x y sc s2].
 
+#[export]
 Hint Extern 20 (Search2 _ _ _) => progress simpl  : typeclass_instances.
 
 Example ex_noalias x1 x2 : def (x2 :-> 1 :+ x1 :-> 2) -> x1 != x2.

theories/perms.v

@@ -256,5 +256,6 @@ Proof. by move=>*; rewrite !catA perm_cat2r. Qed.
 
 End Permutations.
 
+#[export]
 Hint Resolve perm_refl perm_catC perm_cons_catCA
              perm_cons_catAC perm_catAC perm_catCA : core.

theories/prefix.v

@@ -80,4 +80,5 @@ Qed.
 
 End Prefix.
 
+#[export]
 Hint Resolve prefix_refl : core.

theories/prelude.v

@@ -160,6 +160,7 @@ Proof. by move=>pf; rewrite eqc. Qed.
 
 End Coercions.
 
+#[export]
 Hint Resolve jmeq_refl : core.
 Arguments jmeq T [A B] x y.
 Notation "a =jm b" := (jmeq id a b) (at level 50).
@@ -207,6 +208,7 @@ Proof. by move=>pf; rewrite eqc2. Qed.
 
 End Coercions2.
 
+#[export]
 Hint Resolve refl_jmeq2 : core.
 Arguments jmeq2 T [A1 A2 B1 B2] x y.
 

theories/rels.v

@@ -289,6 +289,7 @@ Definition EqPredType_trans r2 r1 r3 := @EqPredType_trans' r1 r2 r3.
 Definition SubPredType_trans r2 r1 r3 := @SubPredType_trans' r1 r2 r3.
 End RelProperties.
 
+#[export]
 Hint Resolve EqPredType_refl SubPredType_refl : core.
 
 (* Declaration of relations *)
@@ -458,6 +459,7 @@ Proof. by move=>H x [H1 H2]; split; [|apply: H]. Qed.
 
 End SubMemLaws.
 
+#[export]
 Hint Resolve subp_refl : core.
 
 Section ListMembership.

theories/stlog.v

@@ -398,12 +398,14 @@ Prenex Implicits swp opn.
 Lemma blah (A : Type) (p : ptr) (l : A) : def (p :-> l) -> (p :-> l) \In p :--> l.
 Proof. by move=>H; apply/swp. Qed.
 
+#[export]
 Hint Immediate blah : core.
 
 Lemma blah2 (A : Type) (v1 v2 : A) q :
         def (q :-> v1) -> v1 = v2 -> q :-> v1 \In q :--> v2.
 Proof. by move=>D E; apply/swp; rewrite E. Qed.
 
+#[export]
 Hint Immediate blah2 : core.
 
 Ltac hauto := (do ?econstructor=>//;

theories/stlogCTC.v

@@ -29,11 +29,13 @@ Arguments update1 [h1 h2 k1 k2].
 Arguments update2 [h1 h2 k1 k2].
 Arguments rest [h1 h2 k1 k2].
 
+#[export]
 Program
 Instance found_struct k1 k2 : Update k1 k2 k1 k2 | 1 := {| rest := empty |}.
 Next Obligation. by rewrite unh0. Qed.
 Next Obligation. by rewrite unh0. Qed.
 
+#[export]
 Program
 Instance left_struct l h1 h2 k1 k2 (f : Update h1 h2 k1 k2) :
   Update (l :+ h1) (l :+ h2) k1 k2 | 2 := {| rest := (l :+ rest f) |}.
@@ -46,6 +48,7 @@ have H : h2 = k2 :+ (rest f) by eapply (update2 f).
 by rewrite -unCA -H.
 Qed.
 
+#[export]
 Program
 Instance right_struct l h1 h2 k1 k2 (f : Update h1 h2 k1 k2) :
   Update (h1 :+ l) (h2 :+ l) k1 k2 | 2 := {| rest := (rest f :+ l) |}.
@@ -95,15 +98,18 @@ End EvalDeallocR.
 Class Find1 (h k : heap) :=
   { rest1 : heap; heq1 : h = k :+ rest1}.
 
+#[export]
 Program
 Instance ffound_struct1 k : Find1 k k | 1 := {| rest1 := empty|}.
 Next Obligation. by rewrite unh0. Qed.
 
+#[export]
 Program
 Instance fleft_struct1 l r k (f : Find1 l k) :
   Find1 (l :+ r) k | 2 := {| rest1 := rest1 :+ r |}.
 Next Obligation. by rewrite unA -heq1.  Qed.
 
+#[export]
 Program
 Instance fright_struct1 l r k (f : Find1 r k) :
   Find1 (l :+ r) k | 2 := {| rest1 :=  l :+ rest1 |}.

theories/stmod.v

@@ -406,6 +406,7 @@ Definition conseq A (s1 s2 : spec A) :=
 Lemma conseq_refl (A : Type) (s : spec A) : conseq s s.
 Proof. by []. Qed.
 
+#[export]
 Hint Resolve conseq_refl : core.
 
 Section Consequence.

theories/stsep.v

@@ -152,6 +152,7 @@ Local Notation conseq1 :=
 Lemma conseq_refl A (s : spec A) : conseq1 A s s.
 Proof. by case: s=>s1 s2 i H; apply: frame0. Qed.
 
+#[export]
 Hint Resolve conseq_refl : core.
 
 Section SepConseq.

theories/xfindCTC.v

@@ -34,15 +34,18 @@ Class XFind A (s : seq A) (e : A) := {
 
 Arguments XFind [A].
 
+#[export]
 Program Instance found_struct A (x:A) t : XFind (x :: t) x := {| seq_of := (x :: t); index_of := 0|}.
 Next Obligation. by split; [|apply: prefix_refl]. Qed.
 
+#[export]
 Program Instance recurse_struct A (y:A) t e (f : XFind t e) :
   XFind (y :: t) e | 2 := {| seq_of := (y :: seq_of); index_of := index_of.+1|}.
 Next Obligation.
 by case:f=>r i /= [H1 H2]; split; [|apply/prefix_cons].
 Qed.
 
+#[export]
 Program Instance extend_struct A (x:A) : XFind [::] x := {| seq_of := [:: x]; index_of := 0|}.
 Next Obligation. by []. Qed.