diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | INSTALL | 4 | ||||
| -rw-r--r-- | README | 12 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 1 | ||||
| -rw-r--r-- | distrib/RELEASE | 2 | ||||
| -rwxr-xr-x | distrib/check-list | 2 | ||||
| -rw-r--r-- | pretyping/termops.ml | 59 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 |
8 files changed, 70 insertions, 13 deletions
@@ -53,6 +53,8 @@ Bug fixes - Fix "Tactic Notation" translation bugs and improve file location of errors - Fix an "omega" bug (may cause "auto with zarith" to succeed more often) - Fix ltac "context" bug on right-hand-side of match clauses +- Fix a printing bug with fixpoints when a notation for products or lambdas + is redefined - Fix "abstract" tactical bug within sections Changes from V8.0beta old syntax to V8.0beta @@ -35,8 +35,8 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). in your $PATH environment variable. To get Coq in native-code, (it runs 4 to 10 times faster than - bytecode, but it takes more time to compile, uses more space), - you will also need the "ocamlopt" (or its native code version + bytecode, but it takes more time to get compiled and the binary is + bigger), you will also need the "ocamlopt" (or its native code version "ocamlopt.opt") command. 2- Check that you have Camlp4 installed on your @@ -66,17 +66,13 @@ THE COQ CLUB. BUGS REPORT. ============ - Send your bug reports by E-mail to + Send your bug reports by filling a form at - coq-bugs@pauillac.inria.fr + http://coq.inria.fr/bin/coq-bugs - or by snail mail to + or by E-mail to - Projet Coq - INRIA Rocquencourt - B.P. 105 - 78153 Le Chesnay - France + coq-bugs@pauillac.inria.fr To be effective, bug reports should mention the Caml version used to compile and run Coq, the Coq version (coqtop -v), the configuration diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index a388605ad..3855ca492 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -308,7 +308,6 @@ and xlate_return_info = function CT_coerce_NONE_to_RETURN_INFO CT_none | (None, Some t) -> CT_return(xlate_formula t) | (Some x, Some t) -> CT_as_and_return(xlate_id_opt_aux x, xlate_formula t) -| (Some Anonymous, None) -> CT_coerce_NONE_to_RETURN_INFO CT_none | (Some _, None) -> assert false and xlate_formula_opt = function diff --git a/distrib/RELEASE b/distrib/RELEASE index 11b795db2..4721bd4bc 100644 --- a/distrib/RELEASE +++ b/distrib/RELEASE @@ -23,7 +23,7 @@ A1) VÉRIFICATIONS - Changement des variables en tête du fichier "configure" et vérification du numéro de versions de OCaml et Camlp4 demandées - - Mise à jour des champs Version, Source et Require dans RH/coq.spec.tpl + - Mise à jour des champs Version, Source et Require dans RH/coq.spec - Mise à jour des dépendances dans debian/control. Ajouter une référence à la version et un "* New upstream version" dans debian/changelog. - Relecture des fichiers "README", "README.win", en particulier, diff --git a/distrib/check-list b/distrib/check-list index be39bc665..711668393 100755 --- a/distrib/check-list +++ b/distrib/check-list @@ -16,7 +16,7 @@ coqdate=`grep "^DATE=" $CONFIGFILE | sed -e 's/^DATE=\(.*\)/\1/'` echo "According to the configure file of the archive to be released" echo " The release version is V$version" -echo " The SearchIsos release version is V$versionsi" +#echo " The SearchIsos release version is V$versionsi" echo " The date is $coqdate" echo echo "Comparing datas with expected ones" diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 6680a2d0e..879ae94d5 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -30,6 +30,65 @@ let print_sort_family = function | InProp -> (str "Prop") | InType -> (str "Type") +let pr_name = function + | Name id -> pr_id id + | Anonymous -> str "_" + +let pr_sp sp = str(string_of_kn sp) + +let rec print_constr c = match kind_of_term c with + | Rel n -> str "#"++int n + | Meta n -> str "Meta(" ++ int n ++ str ")" + | Var id -> pr_id id + | Sort s -> print_sort s + | Cast (c,t) -> hov 1 + (str"(" ++ print_constr c ++ cut() ++ + str":" ++ print_constr t ++ str")") + | Prod (Name(id),t,c) -> hov 1 + (str"forall " ++ pr_id id ++ str":" ++ print_constr t ++ str"," ++ + spc() ++ print_constr c) + | Prod (Anonymous,t,c) -> hov 0 + (str"(" ++ print_constr t ++ str " ->" ++ spc() ++ + print_constr c ++ str")") + | Lambda (na,t,c) -> hov 1 + (str"fun " ++ pr_name na ++ str":" ++ + print_constr t ++ str" =>" ++ spc() ++ print_constr c) + | LetIn (na,b,t,c) -> hov 0 + (str"let " ++ pr_name na ++ str":=" ++ print_constr b ++ + str":" ++ brk(1,2) ++ print_constr t ++ cut() ++ + print_constr c) + | App (c,l) -> hov 1 + (str"(" ++ print_constr c ++ spc() ++ + prlist_with_sep spc print_constr (Array.to_list l) ++ str")") + | Evar (e,l) -> hov 1 + (str"Evar#" ++ int e ++ str"{" ++ + prlist_with_sep spc print_constr (Array.to_list l) ++str"}") + | Const c -> str"Cst(" ++ pr_sp c ++ str")" + | Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")" + | Construct ((sp,i),j) -> + str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" + | Case (ci,p,c,bl) -> v 0 + (hv 0 (str"<"++print_constr p++str">"++ cut() ++ str"Case " ++ + print_constr c ++ str"of") ++ cut() ++ + prlist_with_sep (fun _ -> brk(1,2)) print_constr (Array.to_list bl) ++ + cut() ++ str"end") + | Fix ((t,i),(lna,tl,bl)) -> + let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in + hov 1 + (str"fix " ++ int i ++ spc() ++ str"{" ++ + v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> + pr_name na ++ str"/" ++ int i ++ str":" ++ print_constr ty ++ + cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++ + str"}") + | CoFix(i,(lna,tl,bl)) -> + let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in + hov 1 + (str"cofix " ++ int i ++ spc() ++ str"{" ++ + v 0 (prlist_with_sep spc (fun (na,ty,bd) -> + pr_name na ++ str":" ++ print_constr ty ++ + cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++ + str"}") + (*let current_module = ref empty_dirpath let set_module m = current_module := m*) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index da3033b0c..d6677fdc4 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -23,6 +23,7 @@ val new_sort_in_family : sorts_family -> sorts (* iterators on terms *) val print_sort : sorts -> std_ppcmds val print_sort_family : sorts_family -> std_ppcmds +val print_constr : constr -> std_ppcmds val prod_it : init:types -> (name * types) list -> types val lam_it : init:constr -> (name * types) list -> constr val rel_vect : int -> int -> constr array |