diff options
| -rwxr-xr-x | tools/restore-v7 | 4 | ||||
| -rwxr-xr-x | tools/upgrade-v8 | 8 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 5 | ||||
| -rw-r--r-- | translate/ppconstrnew.ml | 7 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 28 |
5 files changed, 28 insertions, 24 deletions
diff --git a/tools/restore-v7 b/tools/restore-v7 index 1115593ed..ab8845879 100755 --- a/tools/restore-v7 +++ b/tools/restore-v7 @@ -1,8 +1,8 @@ #!/bin/sh echo Restoring v7 files from directory v7 -for i in v7/*.v v7/*/*.v v7/*/*/*.v v7/*/*/*/*.v v7/*/*/*/*/*.v v7/*/*/*/*/*/*.v; do - if expr $i : '.*\*\.v' > /dev/null ; then continue ; fi +v7files=`find v7 -name \*.v` +for i in $v7files; do j=`echo $i | sed -e "s@^v7/@@"` echo Restoring $i from v7 cp -f $i $j diff --git a/tools/upgrade-v8 b/tools/upgrade-v8 index 513df2f22..443e70f26 100755 --- a/tools/upgrade-v8 +++ b/tools/upgrade-v8 @@ -3,8 +3,8 @@ mv v7 v7.bak echo ---------------- Saving v7 files into directory v7 ------------------ -for i in *.v */*.v */*/*.v */*/*/*.v */*/*/*/*.v */*/*/*/*/*.v; do - if expr $i : '.*\*\.v' > /dev/null ; then continue ; fi +vfiles=`find . -name \*.v` +for i in $files; do if expr $i : 'v7\.bak/.*\.v' > /dev/null ; then continue ; fi if expr $i : 'v7/.*\.v' > /dev/null ; then continue ; fi echo Saving $i into v7/$i @@ -14,8 +14,8 @@ for i in *.v */*.v */*/*.v */*/*/*.v */*/*/*/*.v */*/*/*/*/*.v; do done echo ---------------- Upgrading files with v8 syntax --------------------- -for i in *.v8 */*.v8 */*/*.v8 */*/*/*.v8 */*/*/*/*.v8 */*/*/*/*/*.v8; do - if expr $i : '.*\*\.v8' > /dev/null ; then continue ; fi +v8files=`find . -name \*.v8` +for i in $v8files; do j=`dirname $i`/`basename $i .v8`.v echo Upgrading $i mv -u -f $i $j diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b0b26b33c..b325c8b19 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -144,12 +144,11 @@ let rec vernac_com interpfun (loc,com) = | _ -> let fs = States.freeze () in if !translate_file then - msgnl - (pr_comments !comments ++ hov 0 (pr_vernac com) ++ sep_end()) + msgnl (pr_comments !comments ++ hov 0 (pr_vernac com)) else (msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++ - pr_vernac com ++ sep_end())); + pr_vernac com)); States.unfreeze fs)); Constrintern.set_temporary_implicits_in []; Constrextern.set_temporary_implicits_out []; diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 6d3974069..5a47410b2 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -422,8 +422,11 @@ let rec pr inherited a = | CApp (_,(None,a),l) -> pr_app pr a l, lapp | CCases (_,(po,rtntypopt),c,eqns) -> v 0 - (hov 4 (str "match " ++ prlist_with_sep sep_v (pr_case_item pr) c - ++ pr_case_type pr rtntypopt ++ str " with") ++ + (hov 4 (str "match " ++ + hov 0 ( + prlist_with_sep sep_v (pr_case_item pr) c + ++ pr_case_type pr rtntypopt) ++ + str " with") ++ prlist (pr_eqn pr) eqns ++ spc() ++ str "end"), latom | CLetTuple (_,nal,(na,po),c,b) -> diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index f8ece8cea..8935b36b7 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -301,14 +301,12 @@ let pr_binder pr_c ty na = let pr_vbinders l = hv 0 (pr_binders l) -let vars_of_valdecls l = function - | LocalRawAssum (nal,c) -> - List.fold_right (function (_,Name id) -> fun l -> id::l | (_,Anonymous) -> fun l -> l) nal l - | LocalRawDef ((_,Name id),c) -> id::l - | LocalRawDef ((_,Anonymous),_) -> l +let length_of_valdecls n = function + | LocalRawAssum (nal,c) -> List.length nal + n + | LocalRawDef (_,c) -> n+1 -let vars_of_vbinders = - List.fold_left vars_of_valdecls [] +let length_of_vbinders = + List.fold_left length_of_valdecls 0 let vars_of_binder l (nal,_) = List.fold_right (function (_,Name id) -> fun l -> id::l | (_,Anonymous) -> fun l -> l) nal l @@ -493,7 +491,7 @@ let rec pr_vernac = function (* Control *) | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end () ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") - | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc() ++ str s + | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc() ++ str "\"" ++ str s ++ str "\"" | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v | VernacVar id -> pr_id id @@ -599,18 +597,18 @@ let rec pr_vernac = function let bl2,body,ty' = extract_def_binders c ty in (bl2,body, spc() ++ str":" ++ spc () ++ pr_lconstr_env_n (Global.env()) - (List.length (vars_of_vbinders bl @ vars_of_vbinders bl2)) + (length_of_vbinders bl + length_of_vbinders bl2) false (prod_rawconstr ty bl)) in let bindings = pr_ne_sep spc pr_vbinders bl ++ if bl2 = [] then mt() else (spc() ++ pr_binders bl2) in - let vars = vars_of_vbinders bl @ vars_of_vbinders bl2 in + let n = length_of_vbinders bl + length_of_vbinders bl2 in let c',iscast = match d with None -> c, false | Some d -> CCast (dummy_loc,c,d), true in let ppred = Some (pr_reduce red ++ - pr_lconstr_env_n (Global.env()) - (List.length vars) iscast (abstract_rawconstr c' bl)) + pr_lconstr_env_n (Global.env()) n iscast + (abstract_rawconstr c' bl)) in (bindings,ty,ppred) | ProveBody (bl,t) -> @@ -796,7 +794,7 @@ pr_vbinders bl ++ spc()) pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc() ++ pr_type_option (fun c -> spc() ++ pr_lconstr c) type_ ++ pr_decl_notation ntn ++ str" :=" ++ brk(1,1) ++ - pr_lconstr_env_n rec_sign (List.length (vars_of_vbinders bl)) + pr_lconstr_env_n rec_sign (length_of_vbinders bl) true (CCast (dummy_loc,def0,type_0)) in hov 1 (str"Fixpoint" ++ spc() ++ @@ -1059,3 +1057,7 @@ in pr_vernac let pr_vernac = make_pr_vernac Ppconstrnew.pr_constr Ppconstrnew.pr_lconstr +let pr_vernac = function + | VernacSyntax _ | VernacGrammar _ as x -> pr_vernac x + | x -> pr_vernac x ++ sep_end () + |