diff options
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | distrib/Makefile | 1 | ||||
| -rw-r--r-- | distrib/debian/changelog | 3 | ||||
| -rwxr-xr-x | distrib/debian/rules | 4 | ||||
| -rw-r--r-- | kernel/term.ml | 10 | ||||
| -rw-r--r-- | kernel/term.mli | 24 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 6 |
7 files changed, 38 insertions, 12 deletions
@@ -207,7 +207,7 @@ case $reals_opt in case $reals_ans in "N"|"n"|"No"|"NO"|"no") reals=basic;; - *) true;; + *) reals=all;; esac;; yes) true;; esac diff --git a/distrib/Makefile b/distrib/Makefile index 4ee9f0f37..374239ce8 100644 --- a/distrib/Makefile +++ b/distrib/Makefile @@ -319,6 +319,7 @@ prep-deb: ${COQDEBORIG}.tar.gz ${COQPACKAGE}.tar.gz cd deb_build ; tar xzf ../${COQPACKAGE}.tar.gz cp -a debian deb_build/${COQPACKAGE} rm -rf deb_build/${COQPACKAGE}/debian/CVS + date > prep-deb deb: prep-deb cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot -uc -us 2>&1 | tee ../../deb.log diff --git a/distrib/debian/changelog b/distrib/debian/changelog index 6e0a1efc3..727d5264c 100644 --- a/distrib/debian/changelog +++ b/distrib/debian/changelog @@ -1,8 +1,9 @@ coq (7.4-1) unstable; urgency=low * New upstream version. + * Should now build native on ppc (ocaml bug being fixed) - -- Judicael Courant <Judicael.Courant@lri.fr> Fri, 31 Jan 2003 16:51:03 +0100 + -- Judicael Courant <Judicael.Courant@lri.fr> Wed, 25 Jun 2003 09:49:06 +0200 coq (7.3.1-1) unstable; urgency=low diff --git a/distrib/debian/rules b/distrib/debian/rules index d2b7b3b4e..d4e1d3376 100755 --- a/distrib/debian/rules +++ b/distrib/debian/rules @@ -15,14 +15,12 @@ ADDPREF=COQINSTALLPREFIX=${COQPREF} TMAKE=timeout 5300 ${MAKE} MAKEQ=${MAKE} -q -CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq +CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all configure: configure-stamp configure-stamp: dh_testdir ./configure -opt ${CONFIGUREOPTS} || ./configure ${CONFIGUREOPTS} - # on powerpc, we refuse to use the ".opt" compilers - if [ `arch` = ppc ] ; then ./configure ${CONFIGUREOPTS} ; fi touch configure-stamp build: configure-stamp build-stamp diff --git a/kernel/term.ml b/kernel/term.ml index f9a1bed14..736734365 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -996,6 +996,9 @@ let prodn n env b = in prodrec (n,env,b) +(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *) +let compose_prod l b = prodn (List.length l) l b + (* lamn n [xn:Tn;..;x1:T1;Gamma] b = [x1:T1]..[xn:Tn]b *) let lamn n env b = let rec lamrec = function @@ -1005,6 +1008,9 @@ let lamn n env b = in lamrec (n,env,b) +(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *) +let compose_lam l b = lamn (List.length l) l b + let applist (f,l) = mkApp (f, Array.of_list l) let applistc f l = mkApp (f, Array.of_list l) @@ -1013,8 +1019,8 @@ let appvect = mkApp let appvectc f l = mkApp (f,l) -(* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T = - * [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *) +(* to_lambda n (x1:T1)...(xn:Tn)T = + * [x1:T1]...[xn:Tn]T *) let rec to_lambda n prod = if n = 0 then prod diff --git a/kernel/term.mli b/kernel/term.mli index 1e7a6e08e..472ffb2c8 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -80,7 +80,7 @@ val body_of_type : types -> constr (*s Term constructors. *) -(* Constructs a DeBrujin index *) +(* Constructs a DeBrujin index (DB indices begin at 1) *) val mkRel : int -> constr (* Constructs a Variable *) @@ -325,7 +325,6 @@ val mkNamedProd_wo_LetIn : named_declaration -> types -> types val mkLambda_or_LetIn : rel_declaration -> constr -> constr val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr - (*s Other term constructors. *) val abs_implicit : constr -> constr @@ -343,14 +342,28 @@ val appvectc : constr -> constr array -> constr where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *) val prodn : int -> (name * constr) list -> constr -> constr +(* [compose_prod l b] = $(x_1:T_1)..(x_n:T_n)b$ + where $l = [(x_n,T_n);\dots;(x_1,T_1)]$. + Inverse of [decompose_prod]. *) +val compose_prod : (name * constr) list -> constr -> constr + (* [lamn n l b] = $[x_1:T_1]..[x_n:T_n]b$ where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *) val lamn : int -> (name * constr) list -> constr -> constr +(* [compose_lam l b] = $[x_1:T_1]..[x_n:T_n]b$ + where $l = [(x_n,T_n);\dots;(x_1,T_1)]$. + Inverse of [decompose_lam] *) +val compose_lam : (name * constr) list -> constr -> constr + (* [to_lambda n l] - = $[x_1:T_1]...[x_n:T_n](x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$ - where $l = (x_1:T_1)...(x_n:T_n)(x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$ *) + = $[x_1:T_1]...[x_n:T_n]T$ + where $l = (x_1:T_1)...(x_n:T_n)T$ *) val to_lambda : int -> constr -> constr + +(* [to_prod n l] + = $(x_1:T_1)...(x_n:T_n)T$ + where $l = [x_1:T_1]...[x_n:T_n]T$ *) val to_prod : int -> constr -> constr (* pseudo-reduction rule *) @@ -415,6 +428,9 @@ val noccur_with_meta : int -> int -> constr -> bool (*s Relocation and substitution *) +(* [exliftn el c] lifts [c] with lifting [el] *) +val exliftn : Esubst.lift -> constr -> constr + (* [liftn n k c] lifts by [n] indexes above [k] in [c] *) val liftn : int -> int -> constr -> constr diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index c22195945..c8740b930 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -86,7 +86,11 @@ let simplif ist = | [id: (?1 ? ?) |- ?] -> $t_is_conj;Elim id;Do 2 Intro;Clear id | [id: (?1 ? ?) |- ?] -> $t_is_disj;Elim id;Intro;Clear id - | [id0: ?1-> ?2; id1: ?1|- ?] -> Generalize (id0 id1);Intro;Clear id0 + | [id0: ?1-> ?2; id1: ?1|- ?] -> + (* Generalize (id0 id1);Intro;Clear id0 does not work + (see Marco Maggiesi's bug PR#301) + so we instead use Assert and Exact. *) + Assert ?2; [Exact (id0 id1) | Clear id0] | [id: ?1 -> ?2|- ?] -> $t_is_unit;Cut ?2; [Intro;Clear id |