From 9216cffaaa1ef137ef5bdb5b290a930cc6198850 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 21 Feb 2011 17:34:06 +0100 Subject: Imported Upstream version 0.2.pl2 --- AAC_matcher.ml | 347 ++++++++++++++++++++++++++++++++------------------- AAC_search_monad.ml | 5 + AAC_search_monad.mli | 1 + CHANGELOG | 28 +++++ Caveats.v | 19 ++- Makefile | 319 ++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 578 insertions(+), 141 deletions(-) create mode 100644 CHANGELOG create mode 100644 Makefile 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 ## +## .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 + -- cgit v1.2.3