Merge commit 'upstream/0.2.pl2'

6 files changed, 578 insertions, 141 deletions

diff --git a/AAC_matcher.ml b/AAC_matcher.ml
index 47ab840..5d738e0 100644
--- a/AAC_matcher.ml
+++ b/AAC_matcher.ml
@@ -41,6 +41,8 @@ end
 module Debug = AAC_helper.Debug (Control)
 open Debug
 
+module Search = AAC_search_monad 	(* a handle *)
+
 type symbol = int
 type var = int
 type units = (symbol * symbol) list (* from AC/A symbols to the unit *)
@@ -64,7 +66,7 @@ let get_unit units op =
 let is_unit units op unit  = List.mem (op,unit) units
 
 
-open AAC_search_monad
+open Search
 
 type 'a mset = ('a * int) list
 let linear p =
@@ -126,7 +128,11 @@ module Terms : sig
 		 | TUnit of symbol
 		 | TVar of var
 
-		    
+  (** {2 Fresh variables: we provide some functions to pick some fresh variables with respect to a term}  *)
+  val fresh_var_term : t -> int
+  val fresh_var_nfterm : nf_term -> int
+
+		     
   (** {2 Constructors: we ensure that the terms are always
       normalised
      
@@ -175,9 +181,31 @@ end
       | TUnit of symbol
       | TVar of var
 
-
-
-     
+	  
+    (** {2 Picking fresh variables}  *)
+
+    (** [fresh_var_term] picks a fresh variable with respect to a term *)
+    let fresh_var_term t =
+      let rec aux = function
+    	| Dot (_,t1,t2)
+    	| Plus (_,t1,t2) -> max (aux t1) (aux t2)
+    	| Sym (_,v) -> Array.fold_left (fun acc x -> max acc (aux x)) 0 v
+    	| Var v -> assert (v >= 0); v
+    	| Unit _ -> 0
+      in
+      aux t
+	  
+    (**  [fresh_var_nfterm] picks a fresh_variable with respect to a term *)
+    let fresh_var_nfterm t =
+      let rec aux = function
+    	| TAC (_,l) -> List.fold_left (fun acc (x,_) -> max acc (aux x)) 0 l
+    	| TA (_,l)
+    	| TSym (_,l) ->  List.fold_left (fun acc x -> max acc (aux x)) 0 l
+    	| TVar v -> assert (v >= 0); v
+    	| TUnit _ -> 0
+      in
+      aux t
+	  
     (** {2 Constructors: we ensure that the terms are always
 	normalised} *)
       	
@@ -453,20 +481,6 @@ end
   
    open X
 
-   let nullifiable p =
-     let nullable = not strict in
-     let has_unit s =
-     try let _ = get_unit units s in true
-     with NoUnit -> false 
-     in
-     let rec aux = function
-       | TA (s,l) -> has_unit s && List.for_all (aux) l
-       | TAC (s,l) -> has_unit s && List.for_all (fun (x,n) -> aux x) l
-       | TSym _ -> false
-       | TVar _ -> nullable
-       | TUnit _ -> true
-     in aux p
-    
    let print_units ()=
      List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units;
      Printf.printf "\n%!"
@@ -801,7 +815,7 @@ let build_a (current : symbol)
   right_pat p >> left_pat >> (fun p -> return p)
 
 
-let conts (unit : symbol) (l : symbol list) p : t m =
+let conts (hole : t) (l : symbol list) p : t m =
   let p = t_of_term p in
   (* - aller chercher les symboles ac et les symboles a
      - construire pour chaque
@@ -813,24 +827,23 @@ let conts (unit : symbol) (l : symbol list) p : t m =
   let acc =   fail () in
   let acc = List.fold_left
     (fun acc s ->
-      acc >>| return (Plus (s,p,Unit unit))
+      acc >>| return (Plus (s,p,hole))
     ) acc ac in
   let acc =
     List.fold_left
       (fun acc s ->
-	acc >>| return (Dot (s,p,Unit unit)) >>| return (Dot (s,Unit unit,p))
+	acc >>| return (Dot (s,p,hole)) >>| return (Dot (s,hole,p))
       ) acc a
   in acc
 
    
 (**
-
     Return the same thing as subterm :
     - The size of the context
     - The context
     - A collection of substitutions (here == return Subst.empty)
 *)
-let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
+let unit_subterm (t : nf_term) (unit : symbol) (hole : t): (int * t * Subst.t m) m =
   let symbols = List.fold_left
     (fun acc (ac,u) -> if u = unit then ac :: acc else acc ) [] units
   in
@@ -846,15 +859,15 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 		(
 		  match r with
 		    | [p,1] ->
-		      positions p >>| conts unit symbols' p
+		      positions p >>| conts hole symbols' p
 		    | _ ->
-		      mk_TAC' s r >> conts unit symbols'
+		      mk_TAC' s r >> conts hole symbols'
 		) >> build_ac s l	  ))
       | TA (s,l) ->
 	let symbols' = List.filter (fun x -> x <> s) symbols in
 	(
 	  (* first the other symbols, and then the more simple case of
-	     this aprticular symbol *)
+	     this particular symbol *)
 	  a_nondet_middle l >>
 	    (fun (l,m,r) ->
 	      (* meant to break the symmetry *)
@@ -864,23 +877,23 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 		(
 		  match m with
 		    | [p] ->
-		      positions p >>| conts unit symbols' p
+		      positions p >>| conts hole symbols' p
 		    | _ ->
-		      mk_TA' s m >> conts unit symbols'
+		      mk_TA' s m >> conts hole symbols'
 		) >> build_a s l r   ))
 	>>|
 	    (
 	      if List.mem s symbols then
 		begin match l with
 		  | [a] -> assert false
-		  | [a;b] -> build_a s [a] [b] (Unit unit)
+		  | [a;b] -> build_a s [a] [b] (hole)
 		  | _ ->
 		    (* on ne construit que les elements interieurs,
 		       d'ou la disymetrie *)
 		    (Positions.a l >>
 		       (fun (left,p,right) ->
 			 if left = [] then fail () else
-			   (build_a s left right (Dot (s,Unit unit,t_of_term p)))))
+			   (build_a s left right (Dot (s,hole,t_of_term p)))))
 		end
 	      else fail ()
 	    )
@@ -894,7 +907,7 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 		return (Sym (s, Array.of_list (List.rev_append l (p::r))))		  ))
 	  >>|
 	      (
-		conts unit symbols t >>
+		conts hole symbols t >>
 		  (fun (p) ->
 	      	    let l = List.map t_of_term l in
 	      	    let r = List.map t_of_term r in
@@ -903,15 +916,15 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 	  >>|  acc
 	) l (fail())
       | TVar x -> assert false
-      | TUnit x  when x = unit -> return (Unit unit)
-      | TUnit x as t -> conts unit symbols t
+      | TUnit x  when x = unit -> return (hole)
+      | TUnit x as t -> conts hole symbols t
   in
   (positions t
    >>|
        (match t with
-	 | TSym _ -> conts unit symbols t
-	 | TAC (s,l)  -> conts unit symbols t
-	 | TA (s,l)  -> conts unit symbols t
+	 | TSym _ -> conts hole symbols t
+	 | TAC (s,l)  -> conts hole symbols t
+	 | TA (s,l)  -> conts hole symbols t
 	 | _ -> fail())
   )
   >> fun (p) -> return (Terms.size p,p,return Subst.empty)
@@ -919,7 +932,7 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 
 
 
-(************)
+			    (************)
 			    (* Matching *)
 			    (************)
 
@@ -942,8 +955,8 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 
 *)
 
-let matching  =  
-  let rec matching env (p : nf_term) (t: nf_term) : Subst.t AAC_search_monad.m=    
+let matching  :  Subst.t  -> nf_term -> nf_term -> Subst.t Search.m=  
+  let rec matching env (p : nf_term) (t: nf_term) : Subst.t Search.m=    
     match p with
       | TAC (s,l) ->
 	  let l = linear l in
@@ -1040,11 +1053,55 @@ let matching  =
     fun env l r ->
       let _ = debug (Printf.sprintf "pattern :%s\nterm    :%s\n%!" (Terms.sprint_nf_term l) (Terms.sprint_nf_term r)) in
       let m = matching env l r  in
-      let _ = debug (Printf.sprintf "count %i" (AAC_search_monad.count m)) in
+      let _ = debug (Printf.sprintf "count %i" (Search.count m)) in
 	m
 
 
+(** [unitifiable p : Subst.t m] *)
+let unitifiable p : (symbol * Subst.t m) m = 
+  let m = List.fold_left 
+    (fun acc (_,unit) -> acc >>| 
+	let m =  matching Subst.empty p (mk_TUnit unit) in 
+	if Search.is_empty m then 
+	  fail ()
+	else 
+	  begin 
+	    return (unit,m)
+	  end
+    ) (fail ()) units
+  in 
+  m
+;;
+
+let nullifiable p =
+  let nullable = not strict in
+  let has_unit s =
+    try let _ = get_unit units s in true
+    with NoUnit -> false 
+  in
+  let rec aux = function
+    | TA (s,l) -> has_unit s && List.for_all (aux) l
+    | TAC (s,l) -> has_unit s && List.for_all (fun (x,n) -> aux x) l
+    | TSym _ -> false
+    | TVar _ -> nullable
+    | TUnit _ -> true
+  in aux p
 
+let unit_warning p ~nullif ~unitif =
+  assert ((Search.is_empty unitif) || nullif);
+  if not (Search.is_empty unitif)
+  then
+    begin
+      Pp.msg_warning
+	(Pp.str
+	   "[aac_tactics] This pattern can be instanciated to match units, some solutions can be missing");
+    end
+
+;;
+
+  
+
+  
 (***********)
 (* Subterm *)
 (***********)
@@ -1077,101 +1134,131 @@ let matching  =
     serve as heuristics to return "interesting" matchings
 *)
 
-let return_non_empty raw_p m =
-  if is_empty m
-  then
-    fail ()
-  else
-    return (raw_p ,m)
-
-let subterm  (raw_p:t) (raw_t:t): (int * t * Subst.t m) m=
-  let _ = debug (String.make 40 '=') in
-  let p = term_of_t units raw_p in
-  let t = term_of_t units raw_t in    
-  let _ =
-    if nullifiable  p
+  let return_non_empty raw_p m =
+    if is_empty m
     then
-      Pp.msg_warning
-	(Pp.str
-	   "[aac_tactics] This pattern might be nullifiable, some solutions can be missing");
-  in
-
-  let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term p)) in
-  let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term t)) in
-  let filter_right current right (p,m) = 
-    if right = []
-    then return (p,m)
-    else 
-      mk_TAC' current right >>
-	fun t -> return (Plus (current,p,t_of_term t),m)
-  in
-  let filter_middle current left right (p,m) =
-    let right_pat p =
+      fail ()
+    else
+      return (raw_p ,m)
+
+  let subterm  (raw_p:t) (raw_t:t): (int * t * Subst.t m) m=
+    let _ = debug (String.make 40 '=') in
+    let p = term_of_t units raw_p in
+    let t = term_of_t units raw_t in    
+    let nullif = nullifiable p in 
+    let unitif = unitifiable p in 
+    let _ = unit_warning p ~nullif ~unitif in
+    let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term p)) in
+    let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term t)) in
+    let filter_right current right (p,m) = 
       if right = []
-      then return p
-      else
-	mk_TA' current right >>
-	  fun t -> return (Dot (current,p,t_of_term t))
+      then return (p,m)
+      else 
+	mk_TAC' current right >>
+	  fun t -> return (Plus (current,p,t_of_term t),m)
     in
-    let left_pat p=
-      if left = []
-      then return p
-      else
-	mk_TA' current left >>
-	  fun t -> return (Dot (current,t_of_term t,p))
-    in  
-    right_pat p >> left_pat >> (fun p -> return (p,m))
-  in
-  let rec subterm (t:nf_term) : (t * Subst.t m) m=
-    match t with
-      | TAC (s,l) ->
-	((ac_nondet_split_raw l) >>
-	    (fun (left,right) ->
-	      (subterm_AC s left) >> (filter_right s right)
-	    ))
-      | TA (s,l) ->
-	(a_nondet_middle l) >>
-	  (fun (left, middle, right) ->
-	    (subterm_A s middle) >>
-	      (filter_middle s left right)
-	  )
-      | TSym (s, l) ->
-	let init =
-	  return_non_empty raw_p (matching  Subst.empty p t)
-	in
-	tri_fold (fun acc l t r ->
-	  ((subterm  t) >>
-	      (fun (p,m) ->
-		let l = List.map t_of_term l in
-		let r = List.map t_of_term r in
-		let p = Sym (s, Array.of_list (List.rev_append l (p::r))) in
-		return (p,m)
-	      )) >>| acc
-	) l init
-      | TVar x -> assert false
-      | TUnit s -> fail ()
-	
-  and subterm_AC s tl   =
-    match tl with
-	[x,1] -> subterm  x
-      | _ ->
-	mk_TAC' s tl >> fun t ->
-	  return_non_empty raw_p (matching  Subst.empty p t)
-  and subterm_A s  tl =
-    match tl with
-	[x] -> subterm  x
-      | _ ->
-	mk_TA' s tl >>
-	  fun t ->
+    let filter_middle current left right (p,m) =
+      let right_pat p =
+	if right = []
+	then return p
+	else
+	  mk_TA' current right >>
+	    fun t -> return (Dot (current,p,t_of_term t))
+      in
+      let left_pat p=
+	if left = []
+	then return p
+	else
+	  mk_TA' current left >>
+	    fun t -> return (Dot (current,t_of_term t,p))
+      in  
+      right_pat p >> left_pat >> (fun p -> return (p,m))
+    in
+    let rec subterm (t:nf_term) : (t * Subst.t m) m=
+      match t with
+	| TAC (s,l) ->
+	  ((ac_nondet_split_raw l) >>
+	      (fun (left,right) ->
+		(subterm_AC s left) >> (filter_right s right)
+	      ))
+	| TA (s,l) ->
+	  (a_nondet_middle l) >>
+	    (fun (left, middle, right) ->
+	      (subterm_A s middle) >>
+		(filter_middle s left right)
+	    )
+	| TSym (s, l) ->
+	  let init =
 	    return_non_empty raw_p (matching  Subst.empty p t)
-  in
-  match p with
-    | TUnit x ->
-      unit_subterm t x
-    | _ -> (subterm t >> fun (p,m) -> return (Terms.size p,p,m))
+	  in
+	  tri_fold (fun acc l t r ->
+	    ((subterm  t) >>
+		(fun (p,m) ->
+		  let l = List.map t_of_term l in
+		  let r = List.map t_of_term r in
+		  let p = Sym (s, Array.of_list (List.rev_append l (p::r))) in
+		  return (p,m)
+		)) >>| acc
+	  ) l init
+	| TVar x -> assert false
+	(* this case is superseded by the later disjunction *)
+	| TUnit s -> fail () 		
+	  
+    and subterm_AC s tl   =
+      match tl with
+	  [x,1] -> subterm  x
+	| _ ->
+	  mk_TAC' s tl >> fun t ->
+	    return_non_empty raw_p (matching  Subst.empty p t)
+    and subterm_A s  tl =
+      match tl with
+	  [x] -> subterm  x
+	| _ ->
+	  mk_TA' s tl >>
+	    fun t ->
+	      return_non_empty raw_p (matching  Subst.empty p t)
+    in
+    match p with
+      | TUnit unit -> unit_subterm t unit raw_p
+      | _ when not (Search.is_empty unitif) ->
+	let unit_matches = 
+	  Search.fold 
+	    (fun (unit,inst) acc -> 
+	      Search.fold 
+		(fun subst acc' ->
+		 let m = unit_subterm t unit (Subst.instantiate subst raw_p) 
+		 in 
+		 m>>| acc'
+		)
+		inst
+		acc      
+	    ) 
+	    unitif 
+	    (fail ())
+	in
+	let nullifies (t : Subst.t) = 
+	  List.for_all (fun (_,x) -> 
+	    List.exists (fun (_,y) -> Unit y = x ) units 
+	  ) (Subst.to_list t)
+	in 
+	let nonunit_matches = 
+	  subterm t >> 
+	    (
+	      fun (p,m) -> 
+		let m = Search.filter (fun subst -> not( nullifies subst)) m in 
+		if Search.is_empty m 
+		then fail ()
+	      else return (Terms.size p,p,m)
+	    )
+	in
+	  unit_matches >>| nonunit_matches  
+	     
+      | _ -> (subterm t >> fun (p,m) -> return (Terms.size p,p,m))
+
 
  end
 
+
 (* The functions we export, handlers for the previous ones. Some debug
    information also *)
 let subterm ?(strict = false) units raw t =
@@ -1183,7 +1270,7 @@ let subterm ?(strict = false) units raw t =
   let sols = time (M.subterm raw) t "%fs spent in subterm (including matching)\n" in
     debug
       (Printf.sprintf "%i possible solution(s)\n"
-	 (AAC_search_monad.fold (fun (_,_,envm) acc -> count envm + acc) sols 0));
+	 (Search.fold (fun (_,_,envm) acc -> count envm + acc) sols 0));
     sols
 
 
diff --git a/AAC_search_monad.ml b/AAC_search_monad.ml
index b7aabbd..09a6455 100644
--- a/AAC_search_monad.ml
+++ b/AAC_search_monad.ml
@@ -63,3 +63,8 @@ let to_list m = (fold (fun x acc -> x::acc) m [])
  
 let sort f m =
   N (List.map (fun x -> F x) (List.sort f (to_list m)))
+
+(* preserve the structure of the heap *)
+let filter f m =
+  fold (fun x acc -> (if f x then return x else fail ()) >>| acc) m (N [])
+  
diff --git a/AAC_search_monad.mli b/AAC_search_monad.mli
index 093f9d9..7e2a910 100644
--- a/AAC_search_monad.mli
+++ b/AAC_search_monad.mli
@@ -39,3 +39,4 @@ val choose : 'a m -> 'a option
 val to_list : 'a m -> 'a list
 val sort :  ('a -> 'a -> int) -> 'a m -> 'a m
 val is_empty: 'a m -> bool
+val filter : ('a -> bool) -> 'a m -> 'a m 
diff --git a/CHANGELOG b/CHANGELOG
new file mode 100644
index 0000000..84b2aae
--- /dev/null
+++ b/CHANGELOG
@@ -0,0 +1,28 @@
+AAC_tactics 0.2-pl2 :
+-----------------
+
+- Improved the handling of nullifiable patterns.
+
+AAC_tactics 0.2.1 :
+-----------------
+
+- backport of some debian patches (thanks to S. Glondu)
+
+AAC_tactics 0.2 :
+-----------------
+
+- Several operators can share a given unit (like max and plus sharing zero)
+- Added some support to rewrite in inequations (using inequations)
+- Better priting functions for aac_instances
+- Overhauled inference of morphisms and operators :
+  * Lift the previous requirement to have at leat one AC and one A operator
+  * Binary operations are infered before morphisms (hence List.assoc can be recognized as being Associative)
+- Should now be able to handle goal with evars (but this is not unification modulo AC)
+- Added several new instances of Associative and Commutative operators
+- The old syntax to declare AC and A operators is no longer supported
+- The tactics do not abstract the proof they built (was troublesome if evars appeared)
+
+AAC_tactics 0.1 :
+-----------------
+Initial release
+
diff --git a/Caveats.v b/Caveats.v
index 8cef602..0d0d5ca 100644
--- a/Caveats.v
+++ b/Caveats.v
@@ -335,7 +335,8 @@ Goal a+b*c = c.
      *)
 Abort.
 
-(** **** If the pattern is a unit:
+(** **** If the pattern is a unit or can be instanciated to be equal
+   to a unit:
   
    The heuristic is to make the unit appear at each possible position
    in the term, e.g. transforming [a] into [1*a] and [a*1], but this
@@ -351,23 +352,19 @@ Goal a+b+c = c.
   (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*)
 Abort.
 
-(** **** If the pattern is a nullifiable, but not a unit:
-
-   The heuristic is to make units appear around subterms that are
-built with AC or A symbols. Note that this case is relevant only if
-one uses [aacu_rewrite]. *)
-
-Hypothesis H : forall x y, (x+y)*x = x*x + y*x.
+(** *** Another example of the former case is the following, where the hypothesis can be instanciated to be equal to [1] *)
+Hypothesis H : forall x y, (x+y)*x = x*x + y *x.
 Goal a*a+b*a + c = c.
   (** Here, only one solution if we use the aac_instance tactic  *)
   aac_instances <- H.
 
-  (** There are three solutions using aacu_instances (but, here,
+  (** There are 8 solutions using aacu_instances (but, here,
      there are infinitely many different solutions). We miss e.g. [a*a +b*a
      + (x*x + y*x)*c], which seems to be more peculiar. *)
-  aacu_instances <- H. 
-Abort.
+  aacu_instances <- H.
 
+  (** The 7 last solutions are the same as if we were matching [1] *)
+  aacu_instances H1.  Abort.
 
 (** The behavior of the tactic is not satisfying in this case. It is
 still unclear how to handle properly this kind of situation : we plan
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..a56d4b6
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,319 @@
+#############################################################################
+##  v      #                   The Coq Proof Assistant                     ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
+##   \VV/  #                                                               ##
+##    //   #  Makefile automagically generated by coq_makefile V8.3        ##
+#############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -R . AAC_tactics -opt MLIFILES = $(MLFILES:.ml=.mli) 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 -f magic.txt 
+#
+
+# 
+# This Makefile may take 3 arguments passed as environment variables:
+#   - COQBIN to specify the directory where Coq binaries resides;
+#   - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.
+COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g')
+CAMLP4:="$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')"
+ifndef CAMLP4BIN
+  CAMLP4BIN:=$(CAMLBIN)
+endif
+
+CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)
+
+##########################
+#                        #
+# Libraries definitions. #
+#                        #
+##########################
+
+OCAMLLIBS:=
+COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \
+  -I $(COQLIB)/library -I $(COQLIB)/parsing \
+  -I $(COQLIB)/pretyping -I $(COQLIB)/interp \
+  -I $(COQLIB)/proofs -I $(COQLIB)/tactics \
+  -I $(COQLIB)/toplevel \
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+COQLIBS:= -R . AAC_tactics
+COQDOCLIBS:=-R . AAC_tactics
+
+##########################
+#                        #
+# Variables definitions. #
+#                        #
+##########################
+
+ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
+OPT:=
+COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+ifdef CAMLBIN
+  COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)
+endif
+COQC:=$(COQBIN)coqc
+COQDEP:=$(COQBIN)coqdep -c
+GALLINA:=$(COQBIN)gallina
+COQDOC:=$(COQBIN)coqdoc
+COQMKTOP:=$(COQBIN)coqmktop
+CAMLLIB:=$(shell $(CAMLBIN)ocamlc -where)
+CAMLC:=$(CAMLBIN)ocamlc -c -rectypes
+CAMLOPTC:=$(CAMLBIN)ocamlopt -c -rectypes
+CAMLLINK:=$(CAMLBIN)ocamlc -rectypes
+CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes
+GRAMMARS:=grammar.cma
+CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo
+CAMLP4OPTIONS:=
+MLIFILES=$(MLFILES:.ml=.mli)
+PP:=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
+
+###################################
+#                                 #
+# Definition of the "all" target. #
+#                                 #
+###################################
+
+VFILES:=AAC.v\
+  Instances.v\
+  Tutorial.v\
+  Caveats.v
+VOFILES:=$(VFILES:.v=.vo)
+GLOBFILES:=$(VFILES:.v=.glob)
+VIFILES:=$(VFILES:.v=.vi)
+GFILES:=$(VFILES:.v=.g)
+HTMLFILES:=$(VFILES:.v=.html)
+GHTMLFILES:=$(VFILES:.v=.g.html)
+MLFILES:=AAC_coq.ml\
+  AAC_helper.ml\
+  AAC_search_monad.ml\
+  AAC_matcher.ml\
+  AAC_theory.ml\
+  AAC_print.ml\
+  AAC_rewrite.ml
+CMOFILES:=$(MLFILES:.ml=.cmo)
+CMIFILES:=$(MLFILES:.ml=.cmi)
+CMXFILES:=$(MLFILES:.ml=.cmx)
+CMXSFILES:=$(MLFILES:.ml=.cmxs)
+OFILES:=$(MLFILES:.ml=.o)
+
+all: $(VOFILES) $(CMOFILES) $(CMXSFILES) doc\
+  aac_tactics.cmxs\
+  aac_tactics.cmxa\
+  aac_tactics.cma\
+  .depend
+spec: $(VIFILES)
+
+gallina: $(GFILES)
+
+html: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)
+
+gallinahtml: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)
+
+all.ps: $(VFILES)
+	$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all-gal.ps: $(VFILES)
+	$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all.pdf: $(VFILES)
+	$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all-gal.pdf: $(VFILES)
+	$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+
+
+###################
+#                 #
+# Custom targets. #
+#                 #
+###################
+
+doc: $(MLIFILES)
+	mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc
+
+aac_tactics.cmxs: $(CMXFILES)
+	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES)
+
+aac_tactics.cmxa: $(CMXFILES)
+	$(CAMLOPTLINK) -g -a -o aac_tactics.cmxa $(CMXFILES)
+
+aac_tactics.cma: $(CMOFILES)
+	$(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES)
+
+.depend: $(MLIFILES)
+	$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend
+
+####################
+#                  #
+# Special targets. #
+#                  #
+####################
+
+.PHONY: all opt byte archclean clean install depend html
+
+%.cmi: %.mli
+	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
+
+%.cmo: %.ml
+	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<
+
+%.cmx: %.ml
+	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<
+
+%.cmxs: %.ml
+	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<
+
+%.cmo: %.ml4
+	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
+
+%.cmx: %.ml4
+	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
+
+%.cmxs: %.ml4
+	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<
+
+%.ml.d: %.ml
+	$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $(PP) "$<" > "$@"
+
+%.vo %.glob: %.v
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+%.vi: %.v
+	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+%.g: %.v
+	$(GALLINA) $<
+
+%.tex: %.v
+	$(COQDOC) -latex $< -o $@
+
+%.html: %.v %.glob
+	$(COQDOC) -html $< -o $@
+
+%.g.tex: %.v
+	$(COQDOC) -latex -g $< -o $@
+
+%.g.html: %.v %.glob
+	$(COQDOC) -html -g $< -o $@
+
+%.v.d: %.v
+	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+byte:
+	$(MAKE) all "OPT:=-byte"
+
+opt:
+	$(MAKE) all "OPT:=-opt"
+
+install:
+	mkdir -p $(COQLIB)/user-contrib
+	(for i in $(VOFILES); do \
+	 install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
+	 install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
+	 done)
+	(for i in $(CMOFILES); do \
+	 install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
+	 install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
+	 done)
+	(for i in $(CMIFILES); do \
+	 install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
+	 install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
+	 done)
+	(for i in $(CMXSFILES); do \
+	 install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
+	 install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
+	 done)
+
+clean:
+	rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~
+	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)
+	rm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)
+	- rm -rf html
+	- rm -rf doc
+	- rm -f aac_tactics.cmxs
+	- rm -f aac_tactics.cmxa
+	- rm -f aac_tactics.cma
+	- rm -f .depend
+
+archclean:
+	rm -f *.cmx *.o
+
+
+printenv: 
+	@echo CAMLC =	$(CAMLC)
+	@echo CAMLOPTC =	$(CAMLOPTC)
+	@echo CAMLP4LIB =	$(CAMLP4LIB)
+
+.dummy: magic.txt
+	mv -f Makefile Makefile.bak
+	$(COQBIN)coq_makefile -f magic.txt -o Makefile
+
+
+-include $(VFILES:.v=.v.d)
+.SECONDARY: $(VFILES:.v=.v.d)
+
+-include $(MLFILES:.ml=.ml.d)
+.SECONDARY: $(MLFILES:.ml=.ml.d)
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+
+
+# override inadequate coq_makefile auto-regeneration
+Makefile: make_makefile magic.txt files.txt
+	./make_makefile
+
+# We want to keep the proofs in Caveats and the Tutorial
+world: $(VOFILES) doc
+	- mkdir -p html
+	$(COQDOC) -toc -utf8 -html -g $(COQDOCLIBS) -d html $(VFILES)
+	$(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Tutorial.v
+	$(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Caveats.v
+
+# additional dependencies for AAC (since aac_tactics.cmxs/cma are not
+# around the first time we run make, coqdep issues a warning and
+# ignores this dependency)
+# (one can safely select one of theses dependencies according to 
+#  coq' compilation mode--bytecode or native)
+AAC.vo: aac_tactics.cmxa aac_tactics.cmxs aac_tactics.cma
+
+# .depend contains dependencies for .mli files
+-include .depend
+.SECONDARY: .depend
+