coq-community · tchajed · Dec 20, 2018 · Dec 17, 2018 · Dec 17, 2018 · Dec 17, 2018
diff --git a/.gitignore b/.gitignore
@@ -1,16 +1,17 @@
 # build output
-.*.aux
+*.aux
 *.vo
 *.glob
+*.d
 
 # make-related output
-/.coqdeps.d
-/Makefile.coq
-/Makefile.coq.conf
+Makefile.coq
+Makefile.coq.conf
 
 # reification plugin
 *.cmi
 *.cmx
 *.cmxs
-*.ml4.d
 *.o
+*.a
+*.cmxa
diff --git a/_CoqProject b/_CoqProject
@@ -1,55 +1,57 @@
--R . ATBR
--I .
+-R theories ATBR
+-I src
 
 -arg -w -arg +default
 -arg -w -arg -variable-collision
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -undo-batch-mode
 
-Common.v
-BoolView.v
-MyFSets.v
-MyFSetProperties.v
-MyFMapProperties.v
-Numbers.v
-Utils_WF.v
-Force.v
-DisjointSets.v  
-Classes.v
-Reification.v
-Functors.v
-Graph.v
-SemiLattice.v
-Monoid.v
-SemiRing.v
-KleeneAlgebra.v
-Converse.v
-Model_Relations.v
-Model_StdRelations.v
-Model_Languages.v
-Model_RegExp.v
-Model_MinPlus.v
-StrictStarForm.v
-MxGraph.v
-MxSemiLattice.v
-MxSemiRing.v
-MxKleeneAlgebra.v
-MxFunctors.v
-DKA_Definitions.v
-DKA_StateSetSets.v
-DKA_CheckLabels.v
-DKA_Construction.v
-DKA_Epsilon.v
-DKA_Determinisation.v
-DKA_Merge.v
-DKA_DFA_Language.v
-DKA_DFA_Equiv.v
-DecideKleeneAlgebra.v
-StrictKleeneAlgebra.v
-ATBR.v
-ATBR_Matrices.v
-Examples.v
-ChurchRosser.v
-ChurchRosser_Points_vs_Algebraic.v
+src/reify.ml
+src/reification.ml4
+src/reification_plugin.mlpack
 
-reification.ml4
+theories/Common.v
+theories/BoolView.v
+theories/MyFSets.v
+theories/MyFSetProperties.v
+theories/MyFMapProperties.v
+theories/Numbers.v
+theories/Utils_WF.v
+theories/Force.v
+theories/DisjointSets.v  
+theories/Classes.v
+theories/Reification.v
+theories/Functors.v
+theories/Graph.v
+theories/SemiLattice.v
+theories/Monoid.v
+theories/SemiRing.v
+theories/KleeneAlgebra.v
+theories/Converse.v
+theories/Model_Relations.v
+theories/Model_StdRelations.v
+theories/Model_Languages.v
+theories/Model_RegExp.v
+theories/Model_MinPlus.v
+theories/StrictStarForm.v
+theories/MxGraph.v
+theories/MxSemiLattice.v
+theories/MxSemiRing.v
+theories/MxKleeneAlgebra.v
+theories/MxFunctors.v
+theories/DKA_Definitions.v
+theories/DKA_StateSetSets.v
+theories/DKA_CheckLabels.v
+theories/DKA_Construction.v
+theories/DKA_Epsilon.v
+theories/DKA_Determinisation.v
+theories/DKA_Merge.v
+theories/DKA_DFA_Language.v
+theories/DKA_DFA_Equiv.v
+theories/DecideKleeneAlgebra.v
+theories/StrictKleeneAlgebra.v
+theories/ATBR.v
+theories/ATBR_Matrices.v
+theories/Examples.v
+theories/ChurchRosser.v
+theories/ChurchRosser_Points_vs_Algebraic.v
diff --git a/src/reification.ml4 b/src/reification.ml4
@@ -0,0 +1,18 @@
+(**************************************************************************)
+(*  This is part of ATBR, it is distributed under the terms of the        *)
+(*         GNU Lesser General Public License version 3                    *)
+(*              (see file LICENSE for more details)                       *)
+(*                                                                        *)
+(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.               *)
+(**************************************************************************)
+
+(** Generic reification, for the classes from [Classes.v] to the inductives from [Reification.v] *)
+
+DECLARE PLUGIN "reification_plugin"
+
+open Ltac_plugin
+open Reify
+
+(* tactic grammar entries *)
+TACTIC EXTEND kleene_reify [ "kleene_reify" ] -> [ reify_goal Reify.Reification.KA.ops ] END
+TACTIC EXTEND semiring_reify [ "semiring_reify" ] -> [ reify_goal Reify.Reification.Semiring.ops ] END
diff --git a/src/reification_plugin.mlpack b/src/reification_plugin.mlpack
@@ -0,0 +1,2 @@
+Reify
+Reification
diff --git a/reification.ml4 → src/reify.ml b/reification.ml4 → src/reify.ml
@@ -1,22 +1,6 @@
-(**************************************************************************)
-(*  This is part of ATBR, it is distributed under the terms of the        *)
-(*         GNU Lesser General Public License version 3                    *)
-(*              (see file LICENSE for more details)                       *)
-(*                                                                        *)
-(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.               *)
-(**************************************************************************)
-
-(** Generic reification, for the classes from [Classes.v] to the inductives from [Reification.v] *)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
-
 open Constr
 open EConstr
 open Names
-open Ltac_plugin
-
-DECLARE PLUGIN "reification"
 
 (* pick an element in an hashtbl *)
 let hashtbl_pick t = Hashtbl.fold (fun i x -> function None -> Some (i,x) | acc -> acc) t None
@@ -205,7 +189,7 @@ module Tbl : sig
      yielding elements of type [typ], with [def] as default value *)
   val to_env: t -> constr -> constr -> constr
 end = struct
-  type t = ref ((constr*constr*constr) list * int)
+  type t = ((constr*constr*constr) list * int) ref
 
   let create () = ref([],1)
 
@@ -353,8 +337,4 @@ let reify_goal ops =
 	   with e -> Feedback.msg_warning (Printer.pr_leconstr_env env sigma reified); raise e)
 
     | _ -> error "unrecognised goal"
-  end 	
-
-(* tactic grammar entries *)
-TACTIC EXTEND kleene_reify [ "kleene_reify" ] -> [ reify_goal Reification.KA.ops ] END
-TACTIC EXTEND semiring_reify [ "semiring_reify" ] -> [ reify_goal Reification.Semiring.ops ] END
+  end
diff --git a/ATBR.v → theories/ATBR.v b/ATBR.v → theories/ATBR.v
diff --git a/ATBR_Matrices.v → theories/ATBR_Matrices.v b/ATBR_Matrices.v → theories/ATBR_Matrices.v
diff --git a/BoolView.v → theories/BoolView.v b/BoolView.v → theories/BoolView.v
diff --git a/ChurchRosser.v → theories/ChurchRosser.v b/ChurchRosser.v → theories/ChurchRosser.v
diff --git a/ChurchRosser_Points_vs_Algebraic.v → theories/ChurchRosser_Points_vs_Algebraic.v b/ChurchRosser_Points_vs_Algebraic.v → theories/ChurchRosser_Points_vs_Algebraic.v
diff --git a/Classes.v → theories/Classes.v b/Classes.v → theories/Classes.v
diff --git a/Common.v → theories/Common.v b/Common.v → theories/Common.v
diff --git a/Converse.v → theories/Converse.v b/Converse.v → theories/Converse.v
diff --git a/DKA_CheckLabels.v → theories/DKA_CheckLabels.v b/DKA_CheckLabels.v → theories/DKA_CheckLabels.v
@@ -86,7 +86,7 @@ Qed.
 Lemma NumSetEqual_refl: forall x, x [=] x.
 Proof. reflexivity. Qed.
 
-Local Hint Resolve collect_compat' collect_idem collect_com NumSetEqual_refl.
+Local Hint Resolve collect_compat' collect_idem collect_com NumSetEqual_refl : core.
 
 Notation clean := RegExp.Clean.rewrite.
 

diff --git a/DKA_Construction.v → theories/DKA_Construction.v b/DKA_Construction.v → theories/DKA_Construction.v
@@ -164,11 +164,11 @@ Module Algebraic.
   Proof. intros. apply belong_add. trivial. Qed.
   Lemma belong_add_var: forall i j n A s, belong s A -> belong s (add_var i j n A).
   Proof. intros. apply belong_add. trivial. Qed.
-  Local Hint Resolve belong_incr belong_incr' belong_add belong_add_one belong_add_var.
+  Local Hint Resolve belong_incr belong_incr' belong_add belong_add_one belong_add_var : core.
 
   Lemma belong_build: forall a i j A s, belong s A -> belong s (build a i j A).
   Proof. induction a; simpl; intros; auto. Qed.
-  Local Hint Resolve belong_build.
+  Local Hint Resolve belong_build : core.
 
   Lemma add_comm : forall a b i f s t M, add a i f (add b s t M) [=0=] add b s t (add a i f M).
   Proof.
@@ -434,11 +434,11 @@ Module Correctness.
   Proof. intros. destruct A. assumption. Qed.
   Lemma belong_add_var: forall i j n A s, belong s A -> belong s (add_var i j n A).
   Proof. intros. destruct A. assumption. Qed.
-  Local Hint Resolve belong_incr belong_incr' belong_add_one belong_add_var.
+  Local Hint Resolve belong_incr belong_incr' belong_add_one belong_add_var : core.
 
   Lemma belong_build: forall a i j A s, belong s A -> belong s (build a i j A).
   Proof. induction a; simpl; intros; auto. Qed.
-  Local Hint Resolve belong_build.
+  Local Hint Resolve belong_build : core.
 
   Lemma epsilonbrel_add_one: forall i j A s t, 
     epsilonbrel (add_one i j A) s t = epsilonbrel A s t || eq_state_bool i s && eq_state_bool j t.
@@ -527,11 +527,11 @@ Module Correctness.
      destruct A. simpl. num_simpl. apply Max.le_max_l.
      destruct A. simpl. auto.
   Qed.
-  Local Hint Resolve bounded_incr bounded_add_one bounded_add_var.
+  Local Hint Resolve bounded_incr bounded_add_one bounded_add_var : core.
 
   Lemma bounded_build: forall a i j A, belong i A -> belong j A -> bounded A -> bounded (build a i j A).
   Proof. induction a; simpl; intros; auto. Qed.
-  Local Hint Resolve bounded_build.
+  Local Hint Resolve bounded_build : core.
 
   Lemma bounded_empty: bounded empty.
   Proof.
@@ -751,7 +751,7 @@ Transparent equal.
     end.
 
 
-  Local Hint Constructors non_strict.
+  Local Hint Constructors non_strict : core.
   Lemma epsilon_rt_build: forall a i j A s t, 
     bounded A ->
     belong i A -> belong j A ->

diff --git a/DKA_DFA_Equiv.v → theories/DKA_DFA_Equiv.v b/DKA_DFA_Equiv.v → theories/DKA_DFA_Equiv.v
@@ -258,7 +258,7 @@ Section correctness.
     rewrite <- DS.sameclass_equiv.  
     rewrite H; reflexivity.
   Qed.
-  Hint Resolve tarjan_equiv_true.
+  Hint Resolve tarjan_equiv_true : core.
 
   Lemma invariant_prog : forall tarjan x y,
     invariant tarjan ->

diff --git a/DKA_DFA_Language.v → theories/DKA_DFA_Language.v b/DKA_DFA_Language.v → theories/DKA_DFA_Language.v
diff --git a/DKA_Definitions.v → theories/DKA_Definitions.v b/DKA_Definitions.v → theories/DKA_Definitions.v
diff --git a/DKA_Determinisation.v → theories/DKA_Determinisation.v b/DKA_Determinisation.v → theories/DKA_Determinisation.v
@@ -428,7 +428,7 @@ Section S.
   (** we need this lemma to use the [StateSetProps.exists_iff] from the FSet library *)
   Lemma final_compat: SetoidList.compat_bool NumSet.E.eq (fun s => StateSet.mem s finaux).
   Proof.  intros x y H. rewrite H. reflexivity. Qed.
-  Local Hint Resolve final_compat.    
+  Local Hint Resolve final_compat : core.
 
 
   (** two auxiliary lemmas about [table_finals], to obtain the characterisation [mem_table_finals] below *)

diff --git a/DKA_Epsilon.v → theories/DKA_Epsilon.v b/DKA_Epsilon.v → theories/DKA_Epsilon.v
diff --git a/DKA_Merge.v → theories/DKA_Merge.v b/DKA_Merge.v → theories/DKA_Merge.v
diff --git a/DKA_StateSetSets.v → theories/DKA_StateSetSets.v b/DKA_StateSetSets.v → theories/DKA_StateSetSets.v
@@ -86,7 +86,7 @@ Lemma compat_split s: compat_bool StateSet.Equal (fun p => StateSet.mem s p).
 Proof. intros ? ? H. rewrite H. trivial. Qed.
 Lemma compat_negsplit s: compat_bool StateSet.Equal (fun p => negb (StateSet.mem s p)).
 Proof. intros ? ? H. rewrite H. trivial. Qed.
-Local Hint Resolve compat_split compat_negsplit.
+Local Hint Resolve compat_split compat_negsplit : core.
 
 Ltac solve_p1 := intros ? ? H'; rewrite H'; reflexivity.
 

diff --git a/DecideKleeneAlgebra.v → theories/DecideKleeneAlgebra.v b/DecideKleeneAlgebra.v → theories/DecideKleeneAlgebra.v
diff --git a/DisjointSets.v → theories/DisjointSets.v b/DisjointSets.v → theories/DisjointSets.v
@@ -354,7 +354,7 @@ Module PosDisjointSets <: DISJOINTSETS Positive.
       inversion 1; auto. 
     Qed. 
 
-    Hint Resolve repr_inv_In DO_inv_In.   
+    Hint Resolve repr_inv_In DO_inv_In : core.
 
     Lemma D_repr : forall x, D t x O <-> repr t x x. 
     Proof.
@@ -406,7 +406,7 @@ Module PosDisjointSets <: DISJOINTSETS Positive.
       ]. 
   Qed.
 
-  Hint Resolve repr_idem DO_inv_In D_inv_n repr_D D_update update_In repr_inv_In.
+  Hint Resolve repr_idem DO_inv_In D_inv_n repr_D D_update update_In repr_inv_In : core.
   Lemma FEquiv_D : forall t t', FEquiv t t' -> (forall x, D t x O <-> D t' x O).
   Proof. 
     intros . unfold FEquiv in H.
@@ -565,7 +565,7 @@ Module PosDisjointSets <: DISJOINTSETS Positive.
       apply repr_inv_In in repr_b. firstorder.
       eapply rsucc. 2 : eapply IHrepr; auto. map_iff. auto. 
     Qed.
-    Hint Resolve repr_x_inv_upd repr_inv_upd link_lemma_1 link_lemma_2 repr_update_fwd.
+    Hint Resolve repr_x_inv_upd repr_inv_upd link_lemma_1 link_lemma_2 repr_update_fwd : core.
 
     Lemma link_main_lemma :
       forall x y,
@@ -659,7 +659,7 @@ Module PosDisjointSets <: DISJOINTSETS Positive.
   Section WF.
     Definition IsWF t : Prop := bounded (p t) (size t).
     Class WF t: Prop := { wf : IsWF t }.
-    Hint Constructors WF.
+    Hint Constructors WF : core.
 
     Inductive find_spec_decl t x : (num * T) -> Type :=
     | find_spec_1 : forall rx t'

diff --git a/Examples.v → theories/Examples.v b/Examples.v → theories/Examples.v
diff --git a/Force.v → theories/Force.v b/Force.v → theories/Force.v
diff --git a/Functors.v → theories/Functors.v b/Functors.v → theories/Functors.v
diff --git a/Graph.v → theories/Graph.v b/Graph.v → theories/Graph.v
@@ -110,15 +110,15 @@ Section leq.
 End leq.
 
 
-Hint Resolve @equal_refl.
-Hint Immediate @equal_sym.
+Hint Resolve @equal_refl : core.
+Hint Immediate @equal_sym : core.
 
 (* BUG : If we add [equal_refl_fit] as hints, they are added as eapply ...*)
 
-Hint Resolve @equal_refl_f1 @equal_refl_f2.
+Hint Resolve @equal_refl_f1 @equal_refl_f2 : core.
 (* Hint Resolve @equal_refl_f1t @equal_refl_f2t *)
 
-Hint Extern 1 (equal ?A ?B (?f _ ?t) (?f _ ?t)) => apply @equal_refl_f1t.
-Hint Extern 2 (equal ?A ?B (?f _ _ ?t) (?f _ _ ?t)) => apply @equal_refl_f2t.
+Hint Extern 1 (equal ?A ?B (?f _ ?t) (?f _ ?t)) => apply @equal_refl_f1t : core.
+Hint Extern 2 (equal ?A ?B (?f _ _ ?t) (?f _ _ ?t)) => apply @equal_refl_f2t : core.
 
-Hint Extern 3 (_ == _) => apply @xif_compat.
+Hint Extern 3 (_ == _) => apply @xif_compat : core.
diff --git a/KleeneAlgebra.v → theories/KleeneAlgebra.v b/KleeneAlgebra.v → theories/KleeneAlgebra.v
diff --git a/Model_Languages.v → theories/Model_Languages.v b/Model_Languages.v → theories/Model_Languages.v
diff --git a/Model_MinPlus.v → theories/Model_MinPlus.v b/Model_MinPlus.v → theories/Model_MinPlus.v
diff --git a/Model_RegExp.v → theories/Model_RegExp.v b/Model_RegExp.v → theories/Model_RegExp.v
@@ -321,8 +321,8 @@ Module RegExp.
     Proof. 
       induction x; constructor; assumption.
     Qed.
-    Local Hint Resolve sequal_refl.
-    Local Hint Constructors sequal.
+    Local Hint Resolve sequal_refl : core.
+    Local Hint Constructors sequal : core.
 
     Lemma sequal_clean_zero_equiv x : sequal (clean x) zero -> is_zero (clean x) = true.
     Proof.
@@ -381,7 +381,7 @@ Module RegExp.
       | e_star: forall A x x', @eval A A x x' -> @eval A A (RegExp.star x) (x'#)
       | e_var: forall i, eval (RegExp.var i) (unpack (val i)).
       Arguments eval : clear implicits.
-      Local Hint Constructors eval.
+      Local Hint Constructors eval : core.
 
       (** evaluation of erased terms *)
       Lemma eval_erase_feval: forall n m a, eval n m (erase a) (feval a).

diff --git a/Model_Relations.v → theories/Model_Relations.v b/Model_Relations.v → theories/Model_Relations.v
diff --git a/Model_StdRelations.v → theories/Model_StdRelations.v b/Model_StdRelations.v → theories/Model_StdRelations.v
diff --git a/Monoid.v → theories/Monoid.v b/Monoid.v → theories/Monoid.v
diff --git a/MxFunctors.v → theories/MxFunctors.v b/MxFunctors.v → theories/MxFunctors.v
diff --git a/MxGraph.v → theories/MxGraph.v b/MxGraph.v → theories/MxGraph.v
diff --git a/MxKleeneAlgebra.v → theories/MxKleeneAlgebra.v b/MxKleeneAlgebra.v → theories/MxKleeneAlgebra.v
diff --git a/MxSemiLattice.v → theories/MxSemiLattice.v b/MxSemiLattice.v → theories/MxSemiLattice.v
diff --git a/MxSemiRing.v → theories/MxSemiRing.v b/MxSemiRing.v → theories/MxSemiRing.v
diff --git a/MyFMapProperties.v → theories/MyFMapProperties.v b/MyFMapProperties.v → theories/MyFMapProperties.v
diff --git a/MyFSetProperties.v → theories/MyFSetProperties.v b/MyFSetProperties.v → theories/MyFSetProperties.v
diff --git a/MyFSets.v → theories/MyFSets.v b/MyFSets.v → theories/MyFSets.v
diff --git a/Numbers.v → theories/Numbers.v b/Numbers.v → theories/Numbers.v
@@ -499,7 +499,7 @@ Module Positive <: NUM.
             end); subst.
 
   (* and this hints to automatically prove some trivial facts, by reflexivity *)
-  Hint Extern 0 (Pos_as_OTA.compare _ _ = Eq) => apply Pos_as_OT.eq_refl.
+  Hint Extern 0 (Pos_as_OTA.compare _ _ = Eq) => apply Pos_as_OT.eq_refl : core.
 
   Lemma pcompare_prop: forall x y, Pos_as_OTA.compare x y = Eq <-> x = y. 
   Proof. intros. intuition; psubst; trivial. Qed. 

diff --git a/Reification.v → theories/Reification.v b/Reification.v → theories/Reification.v
@@ -99,4 +99,4 @@ Module KA.
   End S.
 End KA.    
 
-Declare ML Module "reification". 
+Declare ML Module "reification_plugin". 
diff --git a/SemiLattice.v → theories/SemiLattice.v b/SemiLattice.v → theories/SemiLattice.v
@@ -23,7 +23,7 @@ Lemma plus_neutral_right `{SemiLattice} A B: forall (x: X A B), x+0 == x.
 Proof. intros. rewrite plus_com; apply plus_neutral_left. Qed.
 
 (** Hints  *)
-Hint Extern 0 (leq _ _ _ _) => apply leq_refl.
+Hint Extern 0 (leq _ _ _ _) => apply leq_refl : core.
 
 Hint Extern 0 (equal _ _ _ _) => first [
     apply plus_assoc
-Original file line number
+Diff line change
@@ Expand Up / @@ -99,4 +99,4 @@ Module KA. @@
       End S.
     End KA.
-    Declare ML Module "reification".
+    Declare ML Module "reification_plugin".