aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--examples/Example.v70
-rw-r--r--src/Conversion_tactics.v308
-rw-r--r--src/SMTCoq.v1
-rw-r--r--src/versions/native/Make1
-rw-r--r--src/versions/native/Makefile1
-rw-r--r--src/versions/standard/Make1
-rw-r--r--src/versions/standard/Makefile11
7 files changed, 387 insertions, 6 deletions
diff --git a/examples/Example.v b/examples/Example.v
index 8138469..2f3ca73 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -68,3 +68,73 @@ Goal forall b1 b2 x1 x2,
Proof.
verit.
Qed.
+
+
+(* Examples of using the conversion tactics *)
+
+Local Open Scope positive_scope.
+
+Goal forall (f : positive -> positive) (x y : positive),
+ implb ((x + 3) =? y)
+ ((f (x + 3)) <=? (f y))
+ = true.
+Proof.
+pos_convert.
+verit.
+Qed.
+
+Goal forall (f : positive -> positive) (x y : positive),
+ implb ((x + 3) =? y)
+ ((3 <? y) && ((f (x + 3)) <=? (f y)))
+ = true.
+Proof.
+pos_convert.
+verit.
+Qed.
+
+Local Close Scope positive_scope.
+
+Local Open Scope N_scope.
+
+Goal forall (f : N -> N) (x y : N),
+ implb ((x + 3) =? y)
+ ((f (x + 3)) <=? (f y))
+ = true.
+Proof.
+N_convert.
+verit.
+Qed.
+
+Goal forall (f : N -> N) (x y : N),
+ implb ((x + 3) =? y)
+ ((2 <? y) && ((f (x + 3)) <=? (f y)))
+ = true.
+Proof.
+N_convert.
+verit.
+Qed.
+
+Local Close Scope N_scope.
+
+Require Import NPeano.
+Local Open Scope nat_scope.
+
+Goal forall (f : nat -> nat) (x y : nat),
+ implb (Nat.eqb (x + 3) y)
+ ((f (x + 3)) <=? (f y))
+ = true.
+Proof.
+nat_convert.
+verit.
+Qed.
+
+Goal forall (f : nat -> nat) (x y : nat),
+ implb (Nat.eqb (x + 3) y)
+ ((2 <? y) && ((f (x + 3)) <=? (f y)))
+ = true.
+Proof.
+nat_convert.
+verit.
+Qed.
+
+Local Close Scope nat_scope. \ No newline at end of file
diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v
new file mode 100644
index 0000000..44ed954
--- /dev/null
+++ b/src/Conversion_tactics.v
@@ -0,0 +1,308 @@
+Require Import ZArith.
+
+(********************************************************************)
+(********************************************************************)
+(* Ces composants sont communs à toutes les tactiques de conversion *)
+(********************************************************************)
+(********************************************************************)
+
+(* SMTCoq utilise Zeq_bool *)
+Lemma Zeq_bool_Zeqb a b : Z.eqb a b = Zeq_bool a b.
+Proof.
+ case_eq (a =? b)%Z.
+ - rewrite Z.eqb_eq. intros ->. symmetry. now rewrite <- Zeq_is_eq_bool.
+ - rewrite Z.eqb_neq. intro H. case_eq (Zeq_bool a b); auto. now rewrite <- Zeq_is_eq_bool.
+Qed.
+
+(* Généralise fun x => f (g x) *)
+Ltac generalize_fun f g :=
+ repeat
+ match goal with
+ | |- context [ f (g ?X) ] => change (f (g X)) with ((fun x => f (g x)) X)
+ end;
+ generalize (fun x => f (g x)).
+
+(* SMTCoq travaille avec les booléens *)
+Lemma implb_impl : forall a b : bool, (implb a b = true -> a = true -> b = true).
+Proof.
+intros a b H.
+destruct a; destruct b; try reflexivity; discriminate.
+Qed.
+
+(****************************)
+(****************************)
+(* Conversion de pos vers Z *)
+(****************************)
+(****************************)
+
+Definition Pos2Z := Zpos.
+
+Definition Z2Pos (z : Z) :=
+ match z with
+ | 0%Z => 1%positive
+ | Zpos p => p
+ | Zneg _ => 1%positive
+ end.
+
+(* Remplace tous les sous-termes p de type positive par Z2Pos (Pos2Z p) *)
+Ltac pos_converting :=
+ (* On crée une variable fraîche de type positive *)
+ let var := fresh "var" in
+ pose proof xH as var;
+ (* Coeur de la tactique *)
+ repeat
+ match goal with
+ (* On capture chaque sous-terme p avec son contexte, i.e. le but est C[p] *)
+ | |- context C[?p] =>
+ (* Si p est de type positive *)
+ match type of p with
+ | positive =>
+ match p with
+ (* Si p est de la forme Z2Pos (Pos2Z _) on abandonne le match car p est déjà réécrit *)
+ | Z2Pos (Pos2Z _) => fail 1
+ (* Il n'est pas nécessaire de réécrire au dessus des symboles connus *)
+ | Pos.add _ _ => fail 1
+ | Pos.mul _ _ => fail 1
+ | _ =>
+ (* Sinon, on analyse la formule obtenue en remplaçant p par notre variable fraîche dans le but *)
+ match context C[var] with
+ (* Si elle contient le terme Z2Pos (Pos2Z var), cela signifie que le contexte C[]
+ est de la forme C'[Z2Pos (Pos2Z [])] et donc on abandonne le match car p est déjà réécrit *)
+ | context [Z2Pos (Pos2Z var)] => fail 1
+ (* Idem: si le contexte contient xO ou xI, c'est qu'on est à l'intérieur d'une constante *)
+ | context [xO var] => fail 1
+ | context [xI var] => fail 1
+ (* Sinon on réécrit *)
+ | _ => change p with (Z2Pos (Pos2Z p))
+ end
+ end
+ end
+ end;
+ (* Finalement, on efface notre variable fraîche *)
+ clear var.
+
+(* Réécrit les opérations et relations de positive vers Z *)
+Ltac pos_rewriting :=
+ repeat
+ match goal with
+ | |-context [Pos.add (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.add (Z2Pos X) (Z2Pos Y)) with (Z2Pos (X + Y))
+ | |-context [Pos.mul (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.mul (Z2Pos X) (Z2Pos Y)) with (Z2Pos (X * Y))
+ | |-context [Pos.ltb (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.ltb (Z2Pos X) (Z2Pos Y)) with (Z.ltb X Y)
+ | |-context [Pos.leb (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.leb (Z2Pos X) (Z2Pos Y)) with (Z.leb X Y)
+ | |-context [Pos.eqb (Z2Pos ?X) (Z2Pos ?Y) ] => change (Pos.eqb (Z2Pos X) (Z2Pos Y)) with (Z.eqb X Y);rewrite Zeq_bool_Zeqb
+ end.
+
+(* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *)
+Lemma pos_is_ltb : forall p : positive, Z.ltb 0 (Pos2Z p) = true.
+Proof. reflexivity. Qed.
+
+(* Réussit si f est un symbole de fonction non interprété *)
+Ltac pos_is_uninterp_fun f :=
+ match f with
+ | xI => fail 1
+ | xO => fail 1
+ | _ => idtac
+ end.
+
+(* Remplace les symbole de fonction et de variables par des versions dans Z
+ et ajoute les hypothèses de positivité *)
+Ltac pos_renaming :=
+ repeat
+ match goal with
+ | |-context [Pos2Z ?X] => is_var X; generalize (pos_is_ltb X); apply implb_impl; generalize (Pos2Z X); clear X; intro X
+ | |-context [?X (Z2Pos ?Y)] => pos_is_uninterp_fun X; generalize_fun X Z2Pos; clear X; intro X
+ | |-context [Pos2Z (?X ?Y)] => pos_is_uninterp_fun X; generalize_fun Pos2Z X; clear X; intro X
+ end;
+ unfold Pos2Z.
+
+(* La tactique complète *)
+Ltac pos_convert := intros; pos_converting; pos_rewriting; pos_renaming.
+
+(**************************)
+(**************************)
+(* Conversion de N vers Z *)
+(**************************)
+(**************************)
+
+Definition N2Z := Z.of_N.
+Definition Z2N := Z.to_N.
+
+(* Remplace tous les sous-termes n de type N par Z2N (N2Z n) *)
+Ltac N_converting :=
+ (* On crée une variable fraîche de type N *)
+ let var := fresh "var" in
+ pose proof N0 as var;
+ (* Coeur de la tactique *)
+ repeat
+ match goal with
+ (* On capture chaque sous-terme n avec son contexte, i.e. le but est C[n] *)
+ | |- context C[?n] =>
+ (* Si n est de type N *)
+ match type of n with
+ | N =>
+ match n with
+ (* Si n est de la forme Z2N (N2Z _) on abandonne le match car n est déjà réécrit *)
+ | Z2N (N2Z _) => fail 1
+ (* Il n'est pas nécessaire de réécrire au dessus des symboles connus *)
+ | N.add _ _ => fail 1
+ | N.mul _ _ => fail 1
+ | _ =>
+ (* Sinon, on analyse la formule obtenue en remplaçant n par notre variable fraîche dans le but *)
+ match context C[var] with
+ (* Si elle contient le terme Z2N (N2Z var), cela signifie que le contexte C[]
+ est de la forme C'[Z2N (N2Z [])] et donc on abandonne le match car n est déjà réécrit *)
+ | context [Z2N (N2Z var)] => fail 1
+ (* Sinon on réécrit *)
+ | _ => replace n with (Z2N (N2Z n)) by apply N2Z.id
+ end
+ end
+ end
+ end;
+ (* Finalement, on efface notre variable fraîche *)
+ clear var.
+
+(* Résoud les hypothèses de positivité lors de la réécriture des opérations *)
+Ltac N_solve_pos := repeat (try apply Z.add_nonneg_nonneg; try apply Z.mul_nonneg_nonneg; try apply N2Z.is_nonneg).
+
+Lemma N_inj_leb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.leb x y = N.leb (Z2N x) (Z2N y).
+Proof. intros; apply Bool.eq_true_iff_eq; rewrite N.leb_le; rewrite Z.leb_le; apply Z2N.inj_le; assumption. Qed.
+
+Lemma N_inj_ltb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.ltb x y = N.ltb (Z2N x) (Z2N y).
+Proof. intros; apply Bool.eq_true_iff_eq; rewrite N.ltb_lt; rewrite Z.ltb_lt; apply Z2N.inj_lt; assumption. Qed.
+
+Lemma N_inj_eqb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.eqb x y = N.eqb (Z2N x) (Z2N y).
+Proof. intros; apply Bool.eq_true_iff_eq; rewrite N.eqb_eq; rewrite Z.eqb_eq; symmetry; apply Z2N.inj_iff; assumption. Qed.
+
+(* Réécrit les opérations et relations de positive vers Z *)
+Ltac N_rewriting :=
+ repeat
+ match goal with
+ | |-context [N.add (Z2N ?X) (Z2N ?Y) ] => replace (N.add (Z2N X) (Z2N Y)) with (Z2N (X + Y)) by (apply Z2N.inj_add; N_solve_pos)
+ | |-context [N.mul (Z2N ?X) (Z2N ?Y) ] => replace (N.mul (Z2N X) (Z2N Y)) with (Z2N (X * Y)) by (apply Z2N.inj_mul; N_solve_pos)
+ | |-context [N.ltb (Z2N ?X) (Z2N ?Y) ] => replace (N.ltb (Z2N X) (Z2N Y)) with (Z.ltb X Y) by (apply N_inj_ltb; N_solve_pos)
+ | |-context [N.leb (Z2N ?X) (Z2N ?Y) ] => replace (N.leb (Z2N X) (Z2N Y)) with (Z.leb X Y) by (apply N_inj_leb; N_solve_pos)
+ | |-context [N.eqb (Z2N ?X) (Z2N ?Y) ] => replace (N.eqb (Z2N X) (Z2N Y)) with (Z.eqb X Y) by (apply N_inj_eqb; N_solve_pos);rewrite Zeq_bool_Zeqb
+ end.
+
+(* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *)
+Lemma N_is_leb : forall n : N, Z.leb 0 (N2Z n) = true.
+Proof. intro; apply Zle_imp_le_bool; apply N2Z.is_nonneg. Qed.
+
+(* Réussit si f est un symbole de fonction non interprété *)
+Ltac N_is_uninterp_fun f :=
+ match f with
+ | Npos => fail 1
+ | _ => idtac
+ end.
+
+(* Remplace les symbole de fonction et de variables par des versions dans Z
+ et ajoute les hypothèses de positivité *)
+Ltac N_renaming :=
+ repeat
+ match goal with
+ | |-context [N2Z ?X] => is_var X; generalize (N_is_leb X); apply implb_impl; generalize (N2Z X); clear X; intro X
+ | |-context [?X (Z2N ?Y)] => N_is_uninterp_fun X; generalize_fun X Z2N; clear X; intro X
+ | |-context [N2Z (?X ?Y)] => N_is_uninterp_fun X; generalize_fun N2Z X; clear X; intro X
+ end;
+ unfold N2Z; simpl.
+
+(* La tactique complète *)
+Ltac N_convert := intros; N_converting; N_rewriting; N_renaming.
+
+(****************************)
+(****************************)
+(* Conversion de nat vers Z *)
+(****************************)
+(****************************)
+
+(* Nécessaire dans native-coq *)
+Require Import NPeano.
+
+Definition Nat2Z := Z.of_nat.
+Definition Z2Nat := Z.to_nat.
+
+(* Remplace tous les sous-termes n de type nat par Z2Nat (Nat2Z n) *)
+Ltac nat_converting :=
+ (* On crée une variable fraîche de type nat *)
+ let var := fresh "var" in
+ pose proof O as var;
+ (* Coeur de la tactique *)
+ repeat
+ match goal with
+ (* On capture chaque sous-terme n avec son contexte, i.e. le but est C[n] *)
+ | |- context C[?n] =>
+ (* Si n est de type nat *)
+ match type of n with
+ | nat =>
+ match n with
+ (* Si n est de la forme Z2Nat (Nat2Z _) on abandonne le match car n est déjà réécrit *)
+ | Z2Nat (Nat2Z _) => fail 1
+ (* Il n'est pas nécessaire de réécrire au dessus des symboles connus *)
+ | Nat.add _ _ => fail 1
+ | Nat.mul _ _ => fail 1
+ | _ =>
+ (* Sinon, on analyse la formule obtenue en remplaçant n par notre variable fraîche dans le but *)
+ match context C[var] with
+ (* Si elle contient le terme Z2Nat (Nat2Z var), cela signifie que le contexte C[]
+ est de la forme C'[Z2Nat (Nat2Z [])] et donc on abandonne le match car n est déjà réécrit *)
+ | context [Z2Nat (Nat2Z var)] => fail 1
+ (* Sinon on réécrit *)
+ | _ => replace n with (Z2Nat (Nat2Z n)) by apply Nat2Z.id
+ end
+ end
+ end
+ end;
+ (* Finalement, on efface notre variable fraîche *)
+ clear var.
+
+(* Résoud les hypothèses de positivité lors de la réécriture des opérations *)
+Ltac nat_solve_pos := repeat (try apply Z.add_nonneg_nonneg; try apply Z.mul_nonneg_nonneg; try apply Nat2Z.is_nonneg).
+
+Lemma nat_inj_leb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.leb x y = Nat.leb (Z2Nat x) (Z2Nat y).
+Proof. intros; apply Bool.eq_true_iff_eq; rewrite Nat.leb_le; rewrite Z.leb_le; apply Z2Nat.inj_le; assumption. Qed.
+
+Lemma nat_inj_ltb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.ltb x y = Nat.ltb (Z2Nat x) (Z2Nat y).
+Proof. intros; apply Bool.eq_true_iff_eq; rewrite Nat.ltb_lt; rewrite Z.ltb_lt; apply Z2Nat.inj_lt; assumption. Qed.
+
+Lemma nat_inj_eqb : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> Z.eqb x y = Nat.eqb (Z2Nat x) (Z2Nat y).
+Proof. intros; apply Bool.eq_true_iff_eq; rewrite Nat.eqb_eq; rewrite Z.eqb_eq; symmetry; apply Z2Nat.inj_iff; assumption. Qed.
+
+(* Réécrit les opérations et relations de positive vers Z *)
+Ltac nat_rewriting :=
+ repeat
+ match goal with
+ | |-context [Nat.add (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.add (Z2Nat X) (Z2Nat Y)) with (Z2Nat (X + Y)) by (apply Z2Nat.inj_add; nat_solve_pos)
+ | |-context [Nat.mul (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.mul (Z2Nat X) (Z2Nat Y)) with (Z2Nat (X * Y)) by (apply Z2Nat.inj_mul; nat_solve_pos)
+ | |-context [Nat.ltb (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.ltb (Z2Nat X) (Z2Nat Y)) with (Z.ltb X Y) by (apply nat_inj_ltb; nat_solve_pos)
+ | |-context [Nat.leb (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.leb (Z2Nat X) (Z2Nat Y)) with (Z.leb X Y) by (apply nat_inj_leb; nat_solve_pos)
+ | |-context [Nat.eqb (Z2Nat ?X) (Z2Nat ?Y) ] => replace (Nat.eqb (Z2Nat X) (Z2Nat Y)) with (Z.eqb X Y) by (apply nat_inj_eqb; nat_solve_pos);rewrite Zeq_bool_Zeqb
+ end.
+
+(* Après avoir converti dans Z il faudra ajouter l'hypothèse de positivité *)
+Lemma nat_is_leb : forall n : nat, Z.leb 0 (Nat2Z n) = true.
+Proof. intro; apply Zle_imp_le_bool; apply Nat2Z.is_nonneg. Qed.
+
+(* Réussit si f est un symbole de fonction non interprété *)
+Ltac nat_is_uninterp_fun f :=
+ match f with
+ | O => fail 1
+ | S => fail 1
+ | _ => idtac
+ end.
+
+(* Remplace les symbole de fonction et de variables par des versions dans Z
+ et ajoute les hypothèses de positivité *)
+Ltac nat_renaming :=
+ repeat
+ match goal with
+ | |-context [Nat2Z ?X] => is_var X; generalize (nat_is_leb X); apply implb_impl; generalize (Nat2Z X); clear X; intro X
+ | |-context [?X (Z2Nat ?Y)] => nat_is_uninterp_fun X; generalize_fun X Z2Nat; clear X; intro X
+ | |-context [Nat2Z (?X ?Y)] => nat_is_uninterp_fun X; generalize_fun Nat2Z X; clear X; intro X
+ end;
+ unfold Nat2Z; simpl.
+
+(* La tactique complète *)
+(* Les "fold" sont nécessaires car dans les anciennes versions de Coq
+ les notations +, *, <? et <=? se réfèrent à plus, mult, ltb et leb
+ et les Nat._ sont définis à partir de plus, mult, ltb et leb. *)
+Ltac nat_convert := fold Nat.add; fold Nat.mul; fold Nat.ltb; fold Nat.leb; fold Nat.eqb; intros; nat_converting; nat_rewriting; nat_renaming.
diff --git a/src/SMTCoq.v b/src/SMTCoq.v
index b6a9871..c7588af 100644
--- a/src/SMTCoq.v
+++ b/src/SMTCoq.v
@@ -16,6 +16,7 @@
Require Export Int63 List PArray.
Require Export State SMT_terms Trace.
+Require Export Conversion_tactics.
Export Atom Form Sat_Checker Cnf_Checker Euf_Checker.
Declare ML Module "smtcoq_plugin".
diff --git a/src/versions/native/Make b/src/versions/native/Make
index 406ebb9..57e85b8 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -111,6 +111,7 @@ spl/Syntactic.v
spl/Arithmetic.v
spl/Operators.v
+Conversion_tactics.v
Misc.v
SMTCoq.v
SMT_terms.v
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index 540b7ce..d443fe9 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -139,6 +139,7 @@ VFILES:=Trace.v\
SMT_terms.v\
SMTCoq.v\
Misc.v\
+ Conversion_tactics.v\
spl/Operators.v\
spl/Arithmetic.v\
spl/Syntactic.v\
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 8defd9b..5322133 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -117,6 +117,7 @@ spl/Syntactic.v
spl/Arithmetic.v
spl/Operators.v
+Conversion_tactics.v
Misc.v
SMTCoq.v
SMT_terms.v
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index 84c10d9..9d2a5de 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -2,7 +2,7 @@
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.6.1 ##
+## // # Makefile automagically generated by coq_makefile V8.6 ##
#############################################################################
# WARNING
@@ -132,7 +132,6 @@ COQSRCLIBS?=-I "$(COQLIB)kernel" \
-I "$(COQLIB)/plugins/firstorder" \
-I "$(COQLIB)/plugins/fourier" \
-I "$(COQLIB)/plugins/funind" \
- -I "$(COQLIB)/plugins/ltac" \
-I "$(COQLIB)/plugins/micromega" \
-I "$(COQLIB)/plugins/nsatz" \
-I "$(COQLIB)/plugins/omega" \
@@ -196,6 +195,7 @@ VFILES:=versions/standard/Int63/Int63.v\
spl/Syntactic.v\
spl/Arithmetic.v\
spl/Operators.v\
+ Conversion_tactics.v\
Misc.v\
SMTCoq.v\
SMT_terms.v\
@@ -502,8 +502,8 @@ uninstall: uninstall_me.sh
@echo "B $(COQLIB)config" >> .merlin
@echo "B $(COQLIB)ltac" >> .merlin
@echo "B $(COQLIB)engine" >> .merlin
- @echo "B /home/artemis/Recherche/Github/smtcoq/smtcoq/src/versions/standard" >> .merlin
- @echo "S /home/artemis/Recherche/Github/smtcoq/smtcoq/src/versions/standard" >> .merlin
+ @echo "B /home/valentin/smtcoq/smtcoq/src/versions/standard" >> .merlin
+ @echo "S /home/valentin/smtcoq/smtcoq/src/versions/standard" >> .merlin
@echo "B cnf" >> .merlin
@echo "S cnf" >> .merlin
@echo "B euf" >> .merlin
@@ -542,7 +542,7 @@ clean::
- rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
cleanall:: clean
- rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
+ rm -f $(patsubst %.v,.%.aux,$(VFILES))
archclean::
rm -f *.cmx *.o
@@ -556,7 +556,6 @@ printenv:
@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
-
###################
# #
# Implicit rules. #
generated by cgit (git 2.34.1) at 2024-06-02 05:59:48 +0000