Imported Upstream version 8.5.1

23 files changed, 212 insertions, 473 deletions

diff --git a/.gitignore b/.gitignore
deleted file mode 100644
index 50cfd07..0000000
--- a/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-doc
-html
diff --git a/AAC.v b/AAC.v
index a16f1a0..f6f382f 100644
--- a/AAC.v
+++ b/AAC.v
@@ -33,6 +33,7 @@ Require Import RelationClasses Equality.
 Require Export Morphisms.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 Local Open Scope signature_scope.
 
diff --git a/CHANGELOG b/CHANGELOG
index 13e9a02..84b2aae 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,8 +1,3 @@
-
-AAC_tactics 0.3 :
------------------
-- New release for Coq 8.4 
-
 AAC_tactics 0.2-pl2 :
 -----------------
 
diff --git a/Caveats.v b/Caveats.v
index d0ec37a..a7967cc 100644
--- a/Caveats.v
+++ b/Caveats.v
@@ -13,7 +13,6 @@
    with the path to the [aac_tactics] library
 *)
 
-Add Rec LoadPath "." as AAC_tactics. 
 Require Import AAC.
 Require Instances.
 
@@ -371,5 +370,3 @@ to investigate on this in the future *)
 
 End Z.
 
-
-
diff --git a/Instances.v b/Instances.v
index 8ddf9e4..55dffbb 100644
--- a/Instances.v
+++ b/Instances.v
@@ -6,6 +6,11 @@
 (*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
 (***************************************************************************)
 
+Require List.
+Require Arith NArith Max Min.
+Require ZArith Zminmax.
+Require QArith Qminmax.
+Require Relations.
 
 Require Export AAC.
 
@@ -19,7 +24,7 @@ Proof. intros x y ->. reflexivity. Qed.
 (* At the moment, all the instances are exported even if they are packaged into modules. Even using LocalInstances in fact*)
 
 Module Peano.
-  Require Import Arith NArith Max Min.
+  Import Arith NArith Max Min.
   Instance aac_plus_Assoc : Associative eq plus := plus_assoc.
   Instance aac_plus_Comm : Commutative eq plus :=  plus_comm.
  
@@ -38,14 +43,14 @@ Module Peano.
 
 
   (* We also provide liftings from le to eq *)
-  Instance preorder_le : PreOrder le := Build_PreOrder _ _ le_refl le_trans.
+  Instance preorder_le : PreOrder le := Build_PreOrder _ le_refl le_trans.
   Instance lift_le_eq : AAC_lift le eq := Build_AAC_lift eq_equivalence _.
 
 End Peano.
 
 
 Module Z.
-  Require Import ZArith Zminmax.
+  Import ZArith Zminmax.
   Open Scope Z_scope.
   Instance aac_Zplus_Assoc : Associative eq Zplus :=  Zplus_assoc.
   Instance aac_Zplus_Comm : Commutative eq Zplus :=  Zplus_comm.
@@ -63,13 +68,13 @@ Module Z.
   Instance aac_zero_Zplus  : Unit eq Zplus 0 := Build_Unit eq Zplus 0 Zplus_0_l Zplus_0_r.
 
   (* We also provide liftings from le to eq *)
-  Instance preorder_Zle : PreOrder Zle := Build_PreOrder _ _ Zle_refl Zle_trans.
+  Instance preorder_Zle : PreOrder Zle := Build_PreOrder _ Zle_refl Zle_trans.
   Instance lift_le_eq : AAC_lift Zle eq := Build_AAC_lift eq_equivalence _.
 
 End Z.
 
 Module Lists.
-   Require Import List.
+   Import List.
    Instance aac_append_Assoc {A} : Associative eq (@app A) := @app_assoc A.
    Instance aac_nil_append  {A} : @Unit (list A) eq (@app A) (@nil A) := Build_Unit _ (@app A) (@nil A) (@app_nil_l A) (@app_nil_r A).
    Instance aac_append_Proper {A} : Proper (eq ==> eq ==> eq) (@app A).
@@ -82,7 +87,7 @@ End Lists.
 
 
 Module N.
-  Require Import NArith.
+  Import NArith.
   Open Scope N_scope.
   Instance aac_Nplus_Assoc : Associative eq Nplus :=  Nplus_assoc.
   Instance aac_Nplus_Comm : Commutative eq Nplus :=  Nplus_comm.
@@ -101,13 +106,13 @@ Module N.
   Instance aac_zero_max  :  Unit eq Nmax 0 := Build_Unit eq Nmax 0 N.max_0_l N.max_0_r. 
    
   (* We also provide liftings from le to eq *)
-  Instance preorder_le : PreOrder Nle := Build_PreOrder _ Nle N.le_refl N.le_trans.
+  Instance preorder_le : PreOrder Nle := Build_PreOrder Nle N.le_refl N.le_trans.
   Instance lift_le_eq : AAC_lift Nle eq := Build_AAC_lift eq_equivalence _.
 
 End N.
 
 Module P.
-  Require Import NArith.
+  Import NArith.
   Open Scope positive_scope.
   Instance aac_Pplus_Assoc : Associative eq Pplus :=  Pplus_assoc.
   Instance aac_Pplus_Comm : Commutative eq Pplus :=  Pplus_comm.
@@ -126,12 +131,12 @@ Module P.
   Instance aac_one_max  :  Unit eq Pmax 1 := Build_Unit eq Pmax 1 Pos.max_1_l Pos.max_1_r. 
 
   (* We also provide liftings from le to eq *)
-  Instance preorder_le : PreOrder Ple := Build_PreOrder _ Ple Pos.le_refl Pos.le_trans.
+  Instance preorder_le : PreOrder Ple := Build_PreOrder Ple Pos.le_refl Pos.le_trans.
   Instance lift_le_eq : AAC_lift Ple eq := Build_AAC_lift eq_equivalence _.
 End P.
 
 Module Q.
-  Require Import QArith Qminmax.
+  Import QArith Qminmax.
   Instance aac_Qplus_Assoc : Associative Qeq Qplus :=  Qplus_assoc.
   Instance aac_Qplus_Comm : Commutative Qeq Qplus :=  Qplus_comm.
  
@@ -148,7 +153,7 @@ Module Q.
   Instance aac_zero_Qplus  : Unit Qeq Qplus 0 := Build_Unit Qeq Qplus 0 Qplus_0_l Qplus_0_r.
 
   (* We also provide liftings from le to eq *)
-  Instance preorder_le : PreOrder Qle := Build_PreOrder _ Qle Qle_refl Qle_trans.
+  Instance preorder_le : PreOrder Qle := Build_PreOrder Qle Qle_refl Qle_trans.
   Instance lift_le_eq : AAC_lift Qle Qeq := Build_AAC_lift QOrderedType.QOrder.TO.eq_equiv _.
 
 End Q.
@@ -162,7 +167,7 @@ Module Prop_ops.
   Instance aac_False : Unit iff and True.  Proof.  constructor; firstorder.  Qed.
  
   Program Instance aac_not_compat : Proper (iff ==> iff) not.
-  Solve All Obligations using firstorder.
+  Solve All Obligations with firstorder.
 
   Instance lift_impl_iff : AAC_lift Basics.impl iff := Build_AAC_lift _  _.
 End Prop_ops.
@@ -179,7 +184,7 @@ Module Bool.
 End Bool.
 
 Module Relations.
-  Require Import Relations.
+  Import Relations.Relations.
   Section defs.
     Variable T : Type.
     Variables R S: relation T.
diff --git a/Make b/Make
new file mode 100644
index 0000000..8caf805
--- /dev/null
+++ b/Make
@@ -0,0 +1,21 @@
+-I .
+-R . AAC_tactics
+coq.mli
+helper.mli
+search_monad.mli
+matcher.mli
+theory.mli
+print.mli
+rewrite.mli
+coq.ml
+helper.ml
+search_monad.ml
+matcher.ml
+theory.ml
+print.ml
+rewrite.ml4
+aac.mlpack
+AAC.v
+Instances.v
+Tutorial.v
+Caveats.v
diff --git a/Makefile b/Makefile
index 03775bc..a9d5466 100644
--- a/Makefile
+++ b/Makefile
@@ -1,34 +1,14 @@
-
-
-FILES := coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli  \
-	evm_compute.mli evm_compute.ml  \
-	 coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 \
-	aac.mlpack \
-	AAC.v  Instances.v Tutorial.v Caveats.v 
-
-ARGS := -R . AAC_tactics
-
-.PHONY: coq clean doc
-
-world: all doc
-
 all: Makefile.coq
-	$(MAKE) -f Makefile.coq all
-
-install: Makefile.coq
-	$(MAKE) -f Makefile.coq install
-
-coq: Makefile.coq
-	$(MAKE) -f Makefile.coq
+	+make -f Makefile.coq all
 
-doc: Makefile.coq
-	$(MAKE) -f Makefile.coq html
-	$(MAKE) -f Makefile.coq mlihtml
+clean: Makefile.coq
+	+make -f Makefile.coq clean
+	rm -f Makefile.coq
 
-Makefile.coq: Makefile $(VS)
-	coq_makefile $(ARGS) $(FILES) -o Makefile.coq
+Makefile.coq: Make
+	$(COQBIN)coq_makefile -f Make -o Makefile.coq
 
-clean:: Makefile.coq
-	$(MAKE) -f Makefile.coq clean
-	rm -f Makefile.coq .depend
+%: Makefile.coq
+	+make -f Makefile.coq $@
 
+.PHONY: all clean
diff --git a/README.txt b/README
index d308f70..38fc514 100644
--- a/README.txt
+++ b/README
@@ -6,8 +6,6 @@
 
 Laboratoire d'Informatique de Grenoble (UMR 5217), INRIA, CNRS, France
 
-Webpage of the project: http://sardes.inrialpes.fr/~braibant/aac_tactics/
-
 
 FOREWORD 
 ======== 
@@ -18,26 +16,8 @@ equations, modulo associativity and commutativity of some operators.
 INSTALLATION
 ============
 
-This plugin should work with Coq v8.4
-
-- running [make] in the top-level directory will generate a Makefile
-  (using coq_makefile), and will build the plugin and its documentation
-
-Option 1
---------
-To install the plugin in Coq's directory, as, e.g., omega or ring.
-
-- run [sudo make install CMXSFILES='aac_tactics.cmxs aac_tactics.cma']
-  to copy the relevant files of the plugin
-
-Option 2
---------
-
-If you chose not to use the previous option, you will need to add the
-following lines to (all) your .v files to be able to use the plugin:
-
-Add Rec LoadPath "absolute_path_to_aac_tactics".
-Add ML Path "absolute_path_to_aac_tactics".
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam install coq-aac-tactics
 
 DOCUMENTATION
 =============
diff --git a/Tutorial.v b/Tutorial.v
index 6356a10..76006ca 100644
--- a/Tutorial.v
+++ b/Tutorial.v
@@ -397,36 +397,3 @@ Section Examples.
 End Examples.
 
 
-Section Match. 
-  (* The following example is inspired by a question by Francois
-  Pottier, wokring in the context of separation logic. *)
-
-  Variable T : Type. 
-  Variable star : T -> T -> T. 
-  Hypothesis P : T -> Prop. 
-
-  Context (starA : Associative eq star).   
-  Context (starC : Commutative eq star).   
-
-  Hypothesis P_hereditary_left : forall a b, P (star a b) -> P a. 
-  Hypothesis P_hereditary_right : forall a b, P (star a b) -> P b. 
-  
-  Notation "a * b" := (star a b). 
-
-  Ltac crush :=
-    match goal with 
-        H: P ?R' |- P ?R =>
-        let h := fresh in
-        aac_match (fun x => x * R) R' h;
-          rewrite <- h in H;
-          try eauto using P_hereditary_right
-    end.    
-
-  Goal forall a b c, P (c * a * c * b) -> P (b * a). 
-  Proof. intros.  crush.  Qed. 
-
-  Goal forall a b c, exists d,  P (d * a * c * b) -> P (b * d) /\ b = d. 
-  Proof. intros.  eexists. intros.  split. crush. reflexivity. Qed. 
-
-End Match. 
-
diff --git a/aac.mlpack b/aac.mlpack
index 60d5298..0c12567 100644
--- a/aac.mlpack
+++ b/aac.mlpack
@@ -4,5 +4,4 @@ Search_monad
 Matcher
 Theory
 Print
-Evm_compute
 Rewrite
diff --git a/coq.ml b/coq.ml
index 132fbf7..97154e2 100644..100755
--- a/coq.ml
+++ b/coq.ml
@@ -19,17 +19,21 @@ let contrib_name = "aac_tactics"
 (* Getting constrs (primitive Coq terms) from existing Coq
    libraries. *)
 let find_constant contrib dir s =
-  Libnames.constr_of_global (Coqlib.find_reference contrib dir s)
+  Universes.constr_of_global (Coqlib.find_reference contrib dir s)
 
 let init_constant dir s = find_constant contrib_name dir s
 
 (* A clause specifying that the [let] should not try to fold anything
    in the goal *)
 let nowhere =
-  { Tacexpr.onhyps = Some [];
-    Tacexpr.concl_occs = Glob_term.no_occurrences_expr
+  { Locus.onhyps = Some [];
+    Locus.concl_occs = Locus.NoOccurrences
   }
 
+let retype c gl =
+  let sigma, _ = Tacmach.pf_apply Typing.type_of gl c in
+    Refiner.tclEVARS sigma gl
+
 let cps_mk_letin
     (name:string)
     (c: constr)
@@ -38,20 +42,20 @@ let cps_mk_letin
   fun goal ->
     let name = (Names.id_of_string name) in
     let name =  Tactics.fresh_id [] name goal in
-    let letin = (Tactics.letin_tac None  (Name name) c None nowhere) in
-      Tacticals.tclTHEN letin (k (mkVar name)) goal
+    let letin = (Proofview.V82.of_tactic (Tactics.letin_tac None  (Name name) c None nowhere)) in
+      Tacticals.tclTHENLIST [retype c; letin; (k (mkVar name))] goal
 
 (** {2 General functions}  *)
 
 type goal_sigma =  Proof_type.goal Tacmach.sigma
 let goal_update (goal : goal_sigma) evar_map : goal_sigma=
   let it = Tacmach.sig_it goal in
-    Tacmach.re_sig it evar_map
+  Tacmach.re_sig it evar_map
 
 let fresh_evar goal ty : constr * goal_sigma =
   let env = Tacmach.pf_env goal in
   let evar_map = Tacmach.project goal in
-  let (em,x) = Evarutil.new_evar evar_map env ty in
+  let (em,x) = Evarutil.new_evar env evar_map ty in
     x,( goal_update goal em)
      
 let resolve_one_typeclass goal ty : constr*goal_sigma=
@@ -69,8 +73,8 @@ let cps_resolve_one_typeclass ?error : Term.types -> (Term.constr  -> Proof_type
 		  try Typeclasses.resolve_one_typeclass env em t
 		  with Not_found ->
 		    begin match error with
-		      | None -> Util.anomaly  "Cannot resolve a typeclass : please report"
-		      | Some x -> Util.error x
+		      | None -> Errors.anomaly (Pp.str "Cannot resolve a typeclass : please report")
+		      | Some x -> Errors.error x
 		    end
 		in
 		Tacticals.tclTHENLIST [Refiner.tclEVARS em; k c] goal
@@ -84,28 +88,28 @@ let nf_evar goal c : Term.constr=
 let evar_unit (gl : goal_sigma) (x : constr) : constr * goal_sigma =
   let env = Tacmach.pf_env gl in
   let evar_map = Tacmach.project gl in
-  let (em,x) = Evarutil.new_evar evar_map env x in
+  let (em,x) = Evarutil.new_evar env evar_map x in
     x,(goal_update gl em)
      
 let evar_binary (gl: goal_sigma) (x : constr) =
   let env = Tacmach.pf_env gl in
   let evar_map = Tacmach.project gl in
   let ty = mkArrow x (mkArrow x x) in
-  let (em,x) = Evarutil.new_evar evar_map env  ty in
+  let (em,x) = Evarutil.new_evar env evar_map ty in
     x,( goal_update gl em)
 
 let evar_relation (gl: goal_sigma) (x: constr) =
   let env = Tacmach.pf_env gl in
   let evar_map = Tacmach.project gl in
   let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in
-  let (em,r) = Evarutil.new_evar evar_map env  ty in
+  let (em,r) = Evarutil.new_evar env evar_map ty in
     r,( goal_update gl em)
 
 let cps_evar_relation (x: constr) k = fun goal -> 
   Tacmach.pf_apply
     (fun env em ->
       let ty = mkArrow x (mkArrow x (mkSort prop_sort)) in
-      let (em,r) = Evarutil.new_evar em env  ty in 	
+      let (em,r) = Evarutil.new_evar env em ty in
       Tacticals.tclTHENLIST [Refiner.tclEVARS em; k r] goal
     )	goal
 
@@ -148,8 +152,6 @@ module Leibniz = struct
   let path = ["Coq"; "Init"; "Logic"]
   let eq_refl = lazy (init_constant path "eq_refl")
   let eq_refl ty x = lapp eq_refl [| ty;x|]
-  let eq ty = Term.mkApp (init_constant path "eq", [| ty |])
-
 end
 
 module Option = struct
@@ -319,7 +321,7 @@ end
 (**[ match_as_equation goal eqt] see [eqt] as an equation. An
    optionnal rel_context can be provided to ensure taht the term
    remains typable*)
-let match_as_equation ?(context = Term.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option  =
+let match_as_equation ?(context = Context.empty_rel_context) goal equation : (constr*constr* Std.Relation.t) option  =
   let env = Tacmach.pf_env goal in
   let env =  Environ.push_rel_context context env in
   let evar_map = Tacmach.project goal in
@@ -330,7 +332,7 @@ let match_as_equation ?(context = Term.empty_rel_context) goal equation : (const
 	let left  =  ca.(n-2) in
 	let right =  ca.(n-1) in
 	let r = (mkApp (c, Array.sub ca 0 (n - 2))) in
-	let carrier =  Typing.type_of env evar_map left in
+	let carrier =  Typing.unsafe_type_of env evar_map left in
 	let rlt =Std.Relation.make carrier r
 	in
 	Some (left, right, rlt )
@@ -359,10 +361,10 @@ let tclPRINT  tac = fun gl ->
 (* functions to handle the failures of our tactic. Some should be
    reported [anomaly], some are on behalf of the user [user_error]*)
 let anomaly msg =
-  Util.anomaly ("[aac_tactics] " ^ msg)
+  Errors.anomaly ~label:"[aac_tactics]" (Pp.str msg)
 
 let user_error msg =
-  Util.error ("[aac_tactics] " ^ msg)
+  Errors.error ("[aac_tactics] " ^ msg)
 
 let warning msg =
   Pp.msg_warning (Pp.str ("[aac_tactics]" ^ msg))
@@ -382,7 +384,7 @@ type hypinfo =
     {
       hyp : Term.constr;		  (** the actual constr corresponding to the hypothese  *)
       hyptype : Term.constr; 		(** the type of the hypothesis *)
-      context : Term.rel_context; 	(** the quantifications of the hypothese *)
+      context : Context.rel_context; 	(** the quantifications of the hypothese *)
       body : Term.constr; 		(** the body of the type of the hypothesis*)
       rel : Std.Relation.t; 		(** the relation  *)
       left : Term.constr;		(** left hand side *)
@@ -391,12 +393,12 @@ type hypinfo =
     }
 
 let get_hypinfo c ~l2r ?check_type  (k : hypinfo -> Proof_type.tactic) :    Proof_type.tactic = fun goal ->
-  let ctype =  Tacmach.pf_type_of goal c in 
+  let ctype =  Tacmach.pf_unsafe_type_of goal c in 
   let (rel_context, body_type) = Term.decompose_prod_assum ctype in 
   let rec check f e =
     match decomp_term e with
       | Term.Rel i ->
-	    let name, constr_option, types = Term.lookup_rel i rel_context
+	    let name, constr_option, types = Context.lookup_rel i rel_context
 	    in f types
       | _ -> Term.fold_constr (fun acc x -> acc && check f x) true e
   in
@@ -441,7 +443,7 @@ let get_hypinfo c ~l2r ?check_type  (k : hypinfo -> Proof_type.tactic) :    Proo
 (* Fresh evars for everyone (should be the good way to do this
    recompose in Coq v8.4) *)
 let recompose_prod 
-    (context : Term.rel_context)
+    (context : Context.rel_context)
     (subst : (int * Term.constr) list)
     env
     em
@@ -462,7 +464,7 @@ let recompose_prod
 	  let em,x =
 	    try em, List.assoc n subst
 	    with | Not_found ->
-	      Evarutil.new_evar em env (Term.substl acc ty)
+	      Evarutil.new_evar env em (Vars.substl acc ty)
 	  in
 	  (Environ.push_rel t env), em,x::acc
 	else
@@ -475,7 +477,7 @@ let recompose_prod
    application to handle non-instanciated variables. *)
    
 let recompose_prod'
-    (context : Term.rel_context)
+    (context : Context.rel_context)
     (subst : (int *Term.constr) list)
     c
     =
@@ -506,7 +508,7 @@ let recompose_prod'
       | None :: sign, _ :: app ->
 	None ::	update sign (List.map (Termops.pop) app)
       | Some decl :: sign, _ :: app ->
-	Some (Term.substl_decl app decl)::update sign (List.map (Termops.pop) app) 
+	Some (Vars.substl_decl app decl)::update sign (List.map (Termops.pop) app) 
   in
   let ctxt = update ctxt app in
   (* updates the rel accordingly, taking some care not to go to far
@@ -576,13 +578,15 @@ let rewrite ?(abort=false)hypinfo subst k =
     (fun rew ->
       let tac =
 	if not abort then
+          Proofview.V82.of_tactic begin
 	  Equality.general_rewrite_bindings
 	    hypinfo.l2r
-	    Termops.all_occurrences
+	    Locus.AllOccurrences
 	    true (* tell if existing evars must be frozen for instantiation *)
 	    false
-	    (rew,Glob_term.NoBindings)
+	    (rew,Misctypes.NoBindings)
 	    true
+          end
 	else
 	  Tacticals.tclIDTAC
       in k tac
diff --git a/coq.mli b/coq.mli
index 53d42eb..1004d2c 100644
--- a/coq.mli
+++ b/coq.mli
@@ -40,6 +40,7 @@ val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Pro
 (** [cps_mk_letin name v] binds the constr [v] using a letin tactic  *)
 val cps_mk_letin : string -> Term.constr -> ( Term.constr -> Proof_type.tactic) -> Proof_type.tactic
 
+val retype : Term.constr -> Proof_type.tactic
 
 val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term
 val lapp : Term.constr lazy_t -> Term.constr array -> Term.constr
@@ -79,7 +80,6 @@ end
 
 module Leibniz : sig
   val eq_refl : Term.types -> Term.constr -> Term.constr
-  val eq : Term.types -> Term.constr
 end
 
 module Option : sig
@@ -149,7 +149,7 @@ end
 (** [match_as_equation ?context goal c] try to decompose c as a
     relation applied to two terms. An optionnal rel_context can be
     provided to ensure that the term remains typable *)
-val match_as_equation  : ?context:Term.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option
+val match_as_equation  : ?context:Context.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option
 
 (** {2 Some tacticials}  *)
 
@@ -190,7 +190,7 @@ type hypinfo =
     {
       hyp : Term.constr;		  (** the actual constr corresponding to the hypothese  *)
       hyptype : Term.constr; 		(** the type of the hypothesis *)
-      context : Term.rel_context; 	(** the quantifications of the hypothese *)
+      context : Context.rel_context; 	(** the quantifications of the hypothese *)
       body : Term.constr; 		(** the body of the hypothese*)
       rel : Relation.t; 		(** the relation  *)
       left : Term.constr;		(** left hand side *)
diff --git a/description b/description
new file mode 100644
index 0000000..7b7195d
--- /dev/null
+++ b/description
@@ -0,0 +1,15 @@
+Name: AACTactics
+Title: AAC tactics
+Description: This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators: 
+Keywords: reflexive tactic, rewriting, rewriting modulo associativity and commutativity, rewriting modulo AC, reflexive decision procedure
+Category: Miscellaneous/Coq Extensions
+Author: Thomas Braibant
+Email: thomas.braibant@gmail.com
+Homepage: http://sardes.inrialpes.fr/~braibant/
+Institution: INRIA/UJF/Ens Lyon
+Author: Damien Pous
+Email: damien.pous@inria.fr
+Homepage: http://sardes.inrialpes.fr/~pous/
+Institution: CNRS
+Require:
+License: LGPL
diff --git a/evm_compute.ml b/evm_compute.ml
deleted file mode 100644
index b10a9cd..0000000
--- a/evm_compute.ml
+++ /dev/null
@@ -1,221 +0,0 @@
-(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmp" i*)
-
-
-let pp_constr fmt x = Pp.pp_with fmt (Printer.pr_constr x)
-let pp_list pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a; " pp x) l
-let pp_list_nl pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a;\n" pp x) l
-let pp_constrs fmt l = (pp_list pp_constr) fmt l
-
-type constr = Term.constr
-
-module Replace (X : sig val eq: Term.constr -> Term.constr -> bool 
-			val subst : (Term.constr * Term.constr) list end) =
-  struct
-
-    (* assumes that [c] and [t] have no outer casts, and all
-       applications have been flattened *)    
-    let rec find l (t: constr) =
-      match l with 
-      | [] -> None
-      | (c,c') :: q -> 
-	begin 
-	  match Term.kind_of_term c, Term.kind_of_term t with 
-	  | Term.App (f1,args1), Term.App (f2, args2) -> 
-	    let l1 = Array.length args1 in 
-	    let l2 = Array.length args2 in 
-	    if l1 <= l2 && X.eq c (Term.mkApp (f2, Array.sub args2 0 l1)) 
-	    then
-	      (* we must return the array of arguments, to make the
-		 substitution in them too *)
-	      Some (c',Array.sub args2 l1 (l2 - l1))
-	    else 
-	      find q t
-	  | _, _ -> 
-	    if X.eq c t 
-	    then Some (c', [| |]) 
-	    else find q t	      
-	end
-	  
-	  
-    let replace_terms t = 
-      let rec aux (k:int) t =
-	match find X.subst t with 
-	| Some (t',v) -> 
-	  let v' = Array.map (Term.map_constr_with_binders (succ) aux k) v in
-	  Term.mkApp (Term.lift k t', v')
-	| None -> 
-	  Term.map_constr_with_binders succ aux k t
-      in aux 0 t
-	  
-  end
-
-let nowhere =
-  { Tacexpr.onhyps = Some [];
-    Tacexpr.concl_occs = Glob_term.no_occurrences_expr
-  }
-
-let mk_letin
-    (name:string)
-    (c: constr)
-    (k : Names .identifier -> Proof_type.tactic)
-: Proof_type.tactic =
-  fun goal ->
-    let name = (Names.id_of_string name) in
-    let name =  Tactics.fresh_id [] name goal in
-    let letin = (Tactics.letin_tac None  (Names.Name name) c None nowhere) in
-      Tacticals.tclTHEN letin (k name) goal
-
-let assert_tac
-    (name:string)
-    (c: constr)
-    (by:Proof_type.tactic)
-    (k : Names.identifier -> Proof_type.tactic)
-: Proof_type.tactic =
-  fun goal ->
-    let name = (Names.id_of_string name) in
-    let name =  Tactics.fresh_id [] name goal in
-    let t = (Tactics.assert_tac  (Names.Name name) c) in
-      Tacticals.tclTHENS t [by; (k name)] goal
-
-
-(* The contrib name is used to locate errors when loading constrs *)
-let contrib_name = "evm_compute"
-
-(* Getting constrs (primitive Coq terms) from existing Coq
-   libraries. *)
-let find_constant contrib dir s =
-  Libnames.constr_of_global (Coqlib.find_reference contrib dir s)
-
-let init_constant dir s = find_constant contrib_name dir s
-
-module Leibniz = struct
-  let path = ["Coq"; "Init"; "Logic"]
-    
-  let eq_refl t x= 
-    Term.mkApp (init_constant path "eq_refl", [| t; x|])
-
-  let eq t x y = 
-    Term.mkApp (init_constant path "eq", [| t; x ; y|])
-      
-  let eq_ind_r ty x p px y yx =
-    Term.mkApp (init_constant path "eq_ind_r", [|ty;x;p;px;y;yx|])
-end
-
-let mk_vm_cast t c = Term.mkCast (c,Term.VMcast,t)
-
-let mk_let  
-    (name:Names.identifier)
-    (c: constr)
-    (t: constr)
-    (k : Names.identifier -> constr) =
-  Term.mkNamedLetIn name c t (Term.subst_vars [name] (k name))
-
-let mk_fun
-    (name:Names.identifier)
-    (t: constr)
-    (k : Names.identifier -> constr) =
-  Term.mkNamedLambda name t (Term.subst_vars [name] (k name))
-
-let rec has_evar x =
-  match Term.kind_of_term x with
-    | Term.Evar _ -> true
-    | Term.Rel _ | Term.Var _ | Term.Meta _ | Term.Sort _ | Term.Const _ | Term.Ind _ | Term.Construct _ ->
-      false
-    | Term.Cast (t1, _, t2) | Term.Prod (_, t1, t2) | Term.Lambda (_, t1, t2) ->
-      has_evar t1 || has_evar t2
-    | Term.LetIn (_, t1, t2, t3) ->
-      has_evar t1 || has_evar t2 || has_evar t3
-    | Term.App (t1, ts) ->
-      has_evar t1 || has_evar_array ts
-    | Term.Case (_, t1, t2, ts) ->
-      has_evar t1 || has_evar t2 || has_evar_array ts
-    | Term.Fix ((_, tr)) | Term.CoFix ((_, tr)) ->
-      has_evar_prec tr
-and has_evar_array x =
-  Util.array_exists has_evar x
-and has_evar_prec (_, ts1, ts2) =
-  Util.array_exists has_evar ts1 || Util.array_exists has_evar ts2
-
-let evm_compute eq blacklist = fun gl -> 
-  (* the type of the conclusion of the goal is [concl] *)
-  let concl = Tacmach.pf_concl gl in 
-
-  let extra = 
-    List.fold_left (fun acc (id,body,ty) -> 
-      match body with 
-	| None -> acc
-	| Some body -> if has_evar body then (Term.mkVar id :: acc) else acc)
-      [] (Tacmach.pf_hyps gl) in 
-
-  (* the set of evars that appear in the goal *)
-  let evars = Evd.evar_list (Tacmach.project gl) concl in 
-  
-  (* the arguments of the function are: the constr that are blacklisted, then the evars  *)
-  let args = extra @ blacklist @ (List.map (fun x -> Term.mkEvar x) evars) in 
-  
-  let argsv = Array.of_list args in 
-
-  let context = (Termops.rel_list 0 (List.length args)) in 
-
-  (* we associate to each argument the proper de bruijn index *)
-  let (subst: (Term.constr * Term.constr) list) = List.combine args context in 
-  
-  let module R = Replace(struct let eq = eq let subst = subst end) in 
-  
-  let t = R.replace_terms concl in 
-  
-  (* we have to retype both the blacklist and the evars to know how to build the final product *)
-  let rel_context = List.map (fun x -> Names.Anonymous, None, Tacmach.pf_type_of gl x) args in 
-  
-  (* the abstraction *)
-  let t = Term.it_mkLambda_or_LetIn t (List.rev rel_context) in 
-  
-  let typeof_t = (Tacmach.pf_type_of gl t) in 
-
-  (* the normal form of the head function *)
-  let nft = Vnorm.cbv_vm (Tacmach.pf_env gl) t typeof_t in 
-  
-
-  let (!!) x = Tactics.fresh_id [] ((Names.id_of_string x)) gl in
-
-  (* p = [fun x => x a_i] which corresponds to the type of the goal when applied to [t] *)
-  let p = mk_fun (!! "x") typeof_t (fun x -> Term.mkApp (Term.mkVar x,argsv)) in 
-  
-  let proof_term pnft = begin  
-    mk_let (!! "nft") nft typeof_t (fun nft -> let nft' = Term.mkVar nft in
-    mk_let (!! "t") t typeof_t (fun t -> let t' = Term.mkVar t in 	
-    mk_let (!! "H") (mk_vm_cast (Leibniz.eq typeof_t t' nft') (Leibniz.eq_refl typeof_t nft')) (Leibniz.eq typeof_t t' nft')
-   (fun h -> 
-    (* typeof_t -> Prop *)
-    let body = Leibniz.eq_ind_r typeof_t 
-      nft' p pnft t' (Term.mkVar h) 
-    in 
-    Term.mkCast (body, Term.DEFAULTcast, Term.mkApp (t', argsv))
-  )))
-  end in 
-  
-  try 
-    assert_tac "subgoal" (Term.mkApp (p,[| nft |]))
-      Tacticals.tclIDTAC
-      (fun subgoal -> 
-	(* We use the tactic [exact_no_check]. It has two consequences:
-	- first, it means that in theory we could produce ill typed proof terms, that fail to type check at Qed; 
-	- second, it means that we are able to use vm_compute and vm_compute casts, that will be checkable at Qed time when all evars have been instantiated. 
-	*)
-	Tactics.exact_no_check (proof_term (Term.mkVar subgoal))  
-      ) gl
-  with 
-    | e ->
-      Tacticals.tclFAIL 0 (Pp.str (Printf.sprintf "evm_compute failed with an exception %s" (Printexc.to_string e))) gl
-      
-;;
-
-let evm_compute_in eq blacklist h = fun gl -> 
-  let concl = Tacmach.pf_concl gl in 
-  Tacticals.tclTHENLIST
-    [Tactics.revert [h];
-     evm_compute eq (concl :: blacklist);
-     Tactics.introduction h
-    ]
-    gl
diff --git a/evm_compute.mli b/evm_compute.mli
deleted file mode 100644
index f50c0db..0000000
--- a/evm_compute.mli
+++ /dev/null
@@ -1,11 +0,0 @@
-
-
-(** [evm_compute eq blacklist] performs a vm_compute step with the
-    following provisos: evars can appear in the goal; terms that are
-    equal (modulo eq) to terms in the blacklist are abstracted
-    before-hand. *)
-val evm_compute : (Term.constr -> Term.constr -> bool) -> Term.constr list -> Proof_type.tactic 
-
-
-(** [evm_compute eq blacklist h] performs an evm_compute step in the hypothesis h *)
-val evm_compute_in : (Term.constr -> Term.constr -> bool) -> Term.constr list -> Names.identifier ->  Proof_type.tactic 
diff --git a/files.txt b/files.txt
deleted file mode 100644
index fb0b175..0000000
--- a/files.txt
+++ /dev/null
@@ -1,11 +0,0 @@
-AAC_coq.ml
-AAC_helper.ml
-AAC_search_monad.ml
-AAC_matcher.ml
-AAC_theory.ml
-AAC_print.ml
-AAC_rewrite.ml
-AAC.v
-Instances.v
-Tutorial.v
-Caveats.v
diff --git a/matcher.ml b/matcher.ml
index 55a64b7..2fd0517 100644
--- a/matcher.ml
+++ b/matcher.ml
@@ -455,7 +455,7 @@ end
        | Dot (s,l,r) -> Dot (s, aux l, aux r)
        | Var i -> 
 	   begin match find t i  with
-	     | None -> Util.error "aac_tactics: instantiate failure"
+	     | None -> Errors.error "aac_tactics: instantiate failure"
 	     | Some x -> t_of_term  x
 	   end
      in aux x
diff --git a/print.ml b/print.ml
index 1ceb786..0305158 100644
--- a/print.ml
+++ b/print.ml
@@ -65,7 +65,7 @@ let pp_all pt : (int * Terms.t * named_env Search_monad.m) Search_monad.m -> Pp.
 rename the variables, and rebuilds raw Coq terms (for the context, and
 the terms in the environment). In order to do so, it requires the
 information gathered by the {!Theory.Trans} module.*)
-let print rlt ir m (context : Term.rel_context) goal =
+let print rlt ir m (context : Context.rel_context) goal =
   if Search_monad.count m = 0
   then
     (
@@ -80,7 +80,7 @@ let print rlt ir m (context : Term.rel_context) goal =
 	  let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in
 	  let l =
 	    List.map (fun (v,t) ->
-	      let (name,body,types) = Term.lookup_rel  v context in
+	      let (name,body,types) = Context.lookup_rel  v context in
 	      (name,t)
 	    ) l
 	  in
diff --git a/print.mli b/print.mli
index 5b3dc15..7fab3be 100644
--- a/print.mli
+++ b/print.mli
@@ -18,6 +18,6 @@ val print :
   Coq.Relation.t ->
   Theory.Trans.ir ->
   (int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m ->
-  Term.rel_context  ->
+  Context.rel_context  ->
   Proof_type.tactic
 
diff --git a/rewrite.ml4 b/rewrite.ml4
index 383d706..b3e52e0 100644
--- a/rewrite.ml4
+++ b/rewrite.ml4
@@ -8,6 +8,7 @@
 
 (** aac_rewrite -- rewriting modulo  *)
 
+DECLARE PLUGIN "aac"
 
 module Control =   struct
     let debug = false
@@ -26,16 +27,15 @@ let tac_or_exn tac exn msg = fun gl ->
     pr_constr "last goal" (Tacmach.pf_concl gl);
     exn msg e
 
+
+let retype = Coq.retype
+
 (* helper to be used with the previous function: raise a new anomaly
    except if a another one was previously raised *)
 let push_anomaly msg = function
-  | Util.Anomaly _ as e -> raise e
+  | e when Errors.is_anomaly e -> raise e
   | _ -> Coq.anomaly msg
 
-
-
-
-
 module M = Matcher
 
 open Term
@@ -184,14 +184,14 @@ let by_aac_reflexivity zero
       (* This convert is required to deal with evars in a proper
 	 way *)
       let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|])   in
-      let convert = Tactics.convert_concl convert_to Term.VMcast in
-      let apply_tac = Tactics.apply decision_thm in
+      let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Term.VMcast) in
+      let apply_tac = Proofview.V82.of_tactic (Tactics.apply decision_thm) in
       (Tacticals.tclTHENLIST
-	 [
+	 [ retype decision_thm; retype convert_to;
 	   convert ;
 	   tac_or_exn apply_tac Coq.user_error "unification failure";
 	   tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) Coq.anomaly "vm_compute failure";
-	   Tacticals.tclORELSE Tactics.reflexivity
+	   Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity)
 	     (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
 	 ])
     )
@@ -215,10 +215,10 @@ let by_aac_normalise zero lift ir t t' =
       (* This convert is required to deal with evars in a proper
 	 way *)
       let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|])   in
-      let convert = Tactics.convert_concl convert_to Term.VMcast in
-      let apply_tac = Tactics.apply normalise_thm in
+      let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Term.VMcast) in
+      let apply_tac = Proofview.V82.of_tactic (Tactics.apply normalise_thm) in
       (Tacticals.tclTHENLIST
-	 [
+	 [ retype normalise_thm; retype convert_to;
 	   convert ;
 	   apply_tac;
 	 ])
@@ -260,6 +260,7 @@ let aac_normalise = fun goal ->
   Tacticals.tclTHENLIST
     [
       aac_conclude by_aac_normalise;
+      Proofview.V82.of_tactic begin
       Tacinterp.interp (
       	<:tactic<
 	  intro x;
@@ -270,8 +271,8 @@ let aac_normalise = fun goal ->
 	  unfold y;
       	  compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl
       	>>
-      );
-      Tactics.keep ids
+      )end;
+      Proofview.V82.of_tactic (Tactics.keep ids)
     ] goal
 
 let aac_reflexivity = fun goal ->
@@ -293,7 +294,8 @@ let aac_reflexivity = fun goal ->
 		   |])
 	  in
 	  Tacticals.tclTHEN
-	    (Tactics.apply lift_reflexivity)
+	  
+	  (Tacticals.tclTHEN (retype lift_reflexivity) (Proofview.V82.of_tactic (Tactics.apply lift_reflexivity)))
 	    (fun goal ->
 	      let concl = Tacmach.pf_concl goal in
 	      let _ = pr_constr "concl "concl in 	     
@@ -330,8 +332,8 @@ let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equ
 	     |])
     in
     Tacticals.tclTHENLIST
-      [
-	Tactics.apply lift_transitivity
+      [ retype lift_transitivity;
+	Proofview.V82.of_tactic (Tactics.apply lift_transitivity)
       ] goal
 
 
@@ -439,41 +441,6 @@ let aac_rewrite  ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
     ) goal
 
 
-(** [aac_match eq (fun x1 ... xn => p) t H] match the term [t] against
-    the pattern, and introduces an hypothesis H of type p = t.  (Note
-    that we have performed the substitution in p).
-*)
-
-let aac_match ~eq pattern term h = fun gl ->
-  let env = Tacmach.pf_env gl in
-  let evar_map = Tacmach.project gl in
-  let carrier = Typing.type_of env evar_map term in   
-  let rel = Coq.Relation.make carrier eq in
-  let equiv,gl = Coq.Equivalence.from_relation gl rel in 
-  (* first, we decompose the pattern as an arity. *)
-  let x_args, pat = Term.decompose_lam pattern in 
-  (* then, we reify the pattern and the term, using the provided equality *)
-  let envs = Theory.Trans.empty_envs () in
-  let left, right,gl = Theory.Trans.t_of_constr gl rel envs (pat,term) in 
-  let gl,ir = Theory.Trans.ir_of_envs gl rel envs in 
-  let solutions = Matcher.matcher (Theory.Trans.ir_to_units ir) left right in 
-  (* then, we pick the first solution   to the matching problem *)
-  let sigma = match Search_monad.choose solutions with
-    | None -> Coq.user_error "no solution to the matching problem"
-    | Some sigma -> sigma
-  in
-  let p_sigma = Matcher.Subst.instantiate sigma left in 
-  let args = List.map (fun (x,t) -> x,Theory.Trans.raw_constr_of_t ir rel [] t) (Matcher.Subst.to_list sigma) in 
-  (* Then, we have to assert the fact that p_sigma is equal to term *)
-  let equation = mkApp (eq, [| Theory.Trans.raw_constr_of_t ir rel [] p_sigma ; term |]) in 
-  let evar_map = Tacmach.project gl in
-  Tacticals.tclTHENLIST 
-    [      
-      Refiner.tclEVARS evar_map;
-      Tactics.assert_by h  equation (by_aac_reflexivity term equiv ir p_sigma right);
-    ] gl
-  
-
 open Coq.Rewrite
 open Tacmach
 open Tacticals
@@ -525,47 +492,39 @@ PRINTED BY pr_constro
 END
 
 TACTIC EXTEND _aac_reflexivity_
-| [ "aac_reflexivity" ] -> [ aac_reflexivity ]
+| [ "aac_reflexivity" ] -> [ Proofview.V82.tactic aac_reflexivity ]
 END
 
 TACTIC EXTEND _aac_normalise_
-| [ "aac_normalise" ] -> [ aac_normalise ]
+| [ "aac_normalise" ] -> [ Proofview.V82.tactic aac_normalise ]
 END
 
 TACTIC EXTEND _aac_rewrite_
 | [ "aac_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
-  [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl ]
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true c gl) ]
 END
  
 TACTIC EXTEND _aac_pattern_
 | [ "aac_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
-  [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl ]
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~abort:true c gl) ]
 END
 
 TACTIC EXTEND _aac_instances_
 | [ "aac_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
-  [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl ]
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:true ~show:true c gl) ]
 END
 
 TACTIC EXTEND _aacu_rewrite_
 | [ "aacu_rewrite" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
-  [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl ]
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false c gl) ]
 END
  
 TACTIC EXTEND _aacu_pattern_
 | [ "aacu_pattern" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
-  [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl ]
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~abort:true c gl) ]
 END
 
 TACTIC EXTEND _aacu_instances_
 | [ "aacu_instances" orient(l2r) constr(c) aac_args(args) constro(extra)] ->
-  [ fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl ]
-END
-
-TACTIC EXTEND _aac_match_
-| [ "aac_match" constr(p) constr(t) ident(h)] ->
-  [ fun gl ->
-    let ty = Tacmach.pf_type_of gl t in 
-    let eq = Coq.Leibniz.eq ty in 
-    aac_match ~eq p t (Names.Name h) gl]
+  [ Proofview.V82.tactic (fun gl -> aac_rewrite ?extra ~args ~l2r ~strict:false ~show:true c gl) ]
 END
diff --git a/rewrite.mli b/rewrite.mli
new file mode 100644
index 0000000..d195075
--- /dev/null
+++ b/rewrite.mli
@@ -0,0 +1,9 @@
+(***************************************************************************)
+(*  This is part of aac_tactics, 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.                *)
+(***************************************************************************)
+
+(** Definition of the tactics, and corresponding Coq grammar entries.*)
diff --git a/theory.ml b/theory.ml
index 3fa35bf..a5229fa 100644
--- a/theory.ml
+++ b/theory.ml
@@ -13,6 +13,7 @@
     be of little interest to most readers.
 *)
 open Term
+open Context
 
 module Control = struct
   let printing = true
@@ -26,15 +27,8 @@ open Debug
 (** {1 HMap :     Specialized Hashtables based on constr} *)
 
 
-module Hashed_constr =
-struct
-  type t = constr
-  let equal = (=)
-  let hash = Hashtbl.hash
-end
-
   (* TODO module HMap = Hashtbl, du coup ? *)
-module HMap = Hashtbl.Make(Hashed_constr)
+module HMap = Hashtbl.Make(Constr)
 
 let ac_theory_path = ["AAC_tactics"; "AAC"]
 
@@ -295,10 +289,10 @@ module Unit = struct
 end
 
 let anomaly msg =
-  Util.anomaly ("aac_tactics: " ^ msg)
+  Errors.anomaly ~label:"aac_tactics" (Pp.str msg)
 
 let user_error msg =
-  Util.error ("aac_tactics: " ^ msg)
+  Errors.error ("aac_tactics: " ^ msg)
 
 module Trans = struct
  
@@ -329,6 +323,64 @@ module Trans = struct
     | Sym of Sym.pack 		
     | Unit of constr  			(* to avoid confusion in bloom *)
 
+  module PackHash =
+  struct
+    open Hashset.Combine
+
+    type t = pack
+
+    let eq_sym_pack p1 p2 =
+      let open Sym in
+      Constr.equal p1.ar p2.ar &&
+      Constr.equal p1.value p2.value &&
+      Constr.equal p1.morph p2.morph
+
+    let hash_sym_pack p =
+      let open Sym in
+      combine3 (Constr.hash p.ar) (Constr.hash p.value) (Constr.hash p.morph)
+
+    let eq_bin_pack p1 p2 =
+      let open Bin in
+      Constr.equal p1.value p2.value &&
+      Constr.equal p1.compat p2.compat &&
+      Constr.equal p1.assoc p2.assoc &&
+      Option.equal Constr.equal p1.comm p2.comm
+
+    let hash_bin_pack p =
+      let open Bin in
+      combine4 (Constr.hash p.value) (Constr.hash p.compat)
+        (Constr.hash p.assoc) (Option.hash Constr.hash p.comm)
+
+    let eq_unit_of u1 u2 =
+      let open Unit in
+      Constr.equal u1.uf_u u2.uf_u &&
+      Constr.equal u1.uf_idx u2.uf_idx &&
+      Constr.equal u1.uf_desc u2.uf_desc
+
+    let hash_unit_of u =
+      let open Unit in
+      combine3 (Constr.hash u.uf_u) (Constr.hash u.uf_idx)
+        (Constr.hash u.uf_desc)
+
+    let equal p1 p2 = match p1, p2 with
+    | Bin (p1, o1), Bin (p2, o2) ->
+      eq_bin_pack p1 p2 && Option.equal eq_unit_of o1 o2
+    | Sym p1, Sym p2 -> eq_sym_pack p1 p2
+    | Unit c1, Unit c2 -> Constr.equal c1 c2
+    | _ -> false
+
+    let hash p = match p with
+    | Bin (p, o) ->
+      combinesmall 1 (combine (hash_bin_pack p) (Option.hash hash_unit_of o))
+    | Sym p ->
+      combinesmall 2 (hash_sym_pack p)
+    | Unit c ->
+      combinesmall 3 (Constr.hash c)
+
+  end
+
+  module PackTable = Hashtbl.Make(PackHash)
+
   (** discr is a map from {!Term.constr} to {!pack}.
      
       [None] means that it is not possible to instantiate this partial
@@ -343,7 +395,7 @@ module Trans = struct
   type envs =
       {
 	discr : (pack option) HMap.t ;
-	bloom : (pack, int ) Hashtbl.t;
+	bloom : int PackTable.t;
 	bloom_back  : (int, pack ) Hashtbl.t;
 	bloom_next : int ref;
       }
@@ -351,7 +403,7 @@ module Trans = struct
   let empty_envs () =
     {
       discr = HMap.create 17;
-      bloom  =  Hashtbl.create 17;
+      bloom  =  PackTable.create 17;
       bloom_back  =  Hashtbl.create 17; 
       bloom_next = ref 1;
     }
@@ -359,16 +411,16 @@ module Trans = struct
           
 
   let add_bloom envs pack =
-    if Hashtbl.mem envs.bloom pack
+    if PackTable.mem envs.bloom pack
     then ()
     else
       let x = ! (envs.bloom_next) in
-	Hashtbl.add envs.bloom pack x;
+	PackTable.add envs.bloom pack x;
 	Hashtbl.add envs.bloom_back x pack;
 	incr (envs.bloom_next)
 
   let find_bloom envs pack =
-    try Hashtbl.find envs.bloom pack
+    try PackTable.find envs.bloom pack
     with Not_found -> assert false
 
   	    (********************************************)
@@ -720,7 +772,7 @@ module Trans = struct
 	    match wu with
 	      | None -> acc
 	      | Some (unit_of) ->
-		let unit_n = Hashtbl.find envs.bloom
+		let unit_n = PackTable.find envs.bloom
 		  (Unit unit_of.Unit.uf_u)
 		in
 		( n,  unit_n)::unit_for,
@@ -742,7 +794,7 @@ module Trans = struct
 		match wu with
 		  | None -> acc
 		  | Some unit_of ->
-		    if unit_of.Unit.uf_u = u
+		    if Constr.equal (unit_of.Unit.uf_u) u
 		    then
 		      {unit_of with
 			Unit.uf_idx = (Coq.Pos.of_int nop)} :: acc
@@ -829,7 +881,7 @@ module Trans = struct
       (** cap rebuilds the products in front of the constr *)
     let rec cap c = function [] -> c
       | t::q -> 
-	  let i = Term.lookup_rel t context in
+	  let i = Context.lookup_rel t context in
 	  cap (mkProd_or_LetIn i c) q
     in
     let t,indices = raw_constr_of_t_debruijn ir t in
diff --git a/theory.mli b/theory.mli
index cc9a617..1dae57b 100644
--- a/theory.mli
+++ b/theory.mli
@@ -160,7 +160,7 @@ module Trans :  sig
       reconstruct the named products on top of it. In particular, this
       allow us to print the context put around the left (or right)
       hand side of a pattern. *)
-  val raw_constr_of_t : ir ->  Coq.Relation.t -> (Term.rel_context)  ->Matcher.Terms.t -> Term.constr
+  val raw_constr_of_t : ir ->  Coq.Relation.t -> (Context.rel_context)  ->Matcher.Terms.t -> Term.constr
 
   (** {2 Building reified terms} *)