diff options
| -rw-r--r-- | parsing/lexer.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 3 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 9 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 3 |
4 files changed, 14 insertions, 2 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 2c17590a3f..0652958c31 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -383,6 +383,7 @@ let rec next_token = parser bp (("METAIDENT", get_buff len), (bp,ep)) | [< ''.' as c; t = parse_after_dot bp c >] ep -> comment_stop bp; + if Options.do_translate() & t=("",".") then between_com := true; (t, (bp,ep)) | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] ep -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 0657765daf..76054c5996 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -617,6 +617,7 @@ let rec pr_atom0 env = function | TacTrivial ([],Some []) -> str "trivial" | TacAuto (None,[],Some []) -> str "auto" | TacReflexivity -> str "reflexivity" + | TacClear (true,[]) -> str "clear" | t -> str "(" ++ pr_atom1 env t ++ str ")" (* Main tactic printer *) @@ -696,6 +697,7 @@ and pr_atom1 env = function | TacNewInduction (h,e,ids) -> hov 1 (str "induction" ++ spc () ++ prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++ + pr_with_names ids ++ pr_opt (pr_eliminator env) e) | TacSimpleDestruct h -> hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) @@ -736,6 +738,7 @@ and pr_atom1 env = function hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ pr_opt int p) (* Context management *) + | TacClear (true,[]) as t -> pr_atom0 env t | TacClear (keep,l) -> hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++ prlist_with_sep spc pr_ident l) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index f43f93bd90..c0aa771ae0 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -828,6 +828,13 @@ and pr_extend s cl = try let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in + let start,rl,cl = + match rl with + | Egrammar.TacTerm s :: rl -> str s, rl, cl + | Egrammar.TacNonTerm _ :: rl -> + (* Will put an unnecessary extra space in front *) + pr_gen (Global.env()) (List.hd cl), rl, List.tl cl + | [] -> anomaly "Empty entry" in let (pp,_) = List.fold_left (fun (strm,args) pi -> @@ -836,7 +843,7 @@ and pr_extend s cl = (strm ++ pr_gen (Global.env()) (List.hd args), List.tl args) | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args)) - (mt(),cl) rl in + (start,cl) rl in hov 1 pp with Not_found -> hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")") diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 6017115c46..665a7bd752 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -34,7 +34,8 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient END (* For Setoid rewrite *) -let pr_morphism_signature _ _ _ = Setoid_replace.pr_morphism_signature +let pr_morphism_signature _ _ _ s = + spc () ++ Setoid_replace.pr_morphism_signature s ARGUMENT EXTEND morphism_signature TYPED AS morphism_signature |