Commit f1943861 authored by MARCHE Claude's avatar MARCHE Claude

cleaning before install

parent f374ae6a
......@@ -212,9 +212,12 @@ clean::
# installation
###############
clean_old_install:
rm -f $(BINDIR)/why3*
rm -rf $(DATADIR)/why3
install_no_local::
mkdir -p $(BINDIR)
rm -rf $(DATADIR)/why3
mkdir -p $(DATADIR)/why3
mkdir -p $(DATADIR)/why3/images
mkdir -p $(DATADIR)/why3/images/boomy
......@@ -251,7 +254,7 @@ install install-lib:
@echo "Why is configured in local installation mode."
@echo "To install Why, run ./configure --disable-local ; make ; make install"
else
install: install_no_local
install: clean_old_install install_no_local
install-lib: install_no_local_lib
endif
......
prelude "(* This file is generated by Why3's Coq driver *)"
prelude "(* This file is generated by Why3's Coq-realize driver *)"
prelude "(* Beware! Only edit allowed sections below *)"
printer "coq-realize"
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -9,7 +9,7 @@ Lemma predicate_extensionality:
forall A (P Q : A -> Prop),
(forall x, P x <-> Q x) -> P = Q.
Admitted.
(* "it is folklore that the two are consistent" *)
(* "it is folklore that the two together are consistent" *)
(* Why3 goal *)
Definition set : forall (a:Type) {a_WT:WhyType a}, Type.
......@@ -17,10 +17,10 @@ intros.
exact (a -> Prop).
Defined.
Global Instance set_WhyType : forall a {a_WT:WhyType a}, WhyType (set a).
Global Instance set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Proof.
intros.
exact (fun _ => True).
exact (fun _ => False).
Qed.
(* Why3 goal *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment