diff options
author | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:15:08 -0400 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:17:55 -0400 |
commit | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch) | |
tree | c413c5bb42d20daf5307634ae6402526bb994fd6 /parsing/ppvernac.ml | |
parent | b9f47391f7f259c24119d1de0a87839e2cc5e80c (diff) |
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'parsing/ppvernac.ml')
-rw-r--r-- | parsing/ppvernac.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 83fcff7e..ff35be57 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ppvernac.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Names @@ -113,7 +113,9 @@ let pr_set_entry_type = function | ETConstr _ -> str"constr" | ETOther (_,e) -> str e | ETBigint -> str "bigint" - | ETConstrList _ -> failwith "Internal entry type" + | ETBinder true -> str "binder" + | ETBinder false -> str "closed binder" + | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" let strip_meta id = let s = string_of_id id in @@ -330,6 +332,14 @@ let pr_onescheme (idop,schem) = hov 0 ((if dep then str"Induction for" else str"Minimality for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) + | CaseScheme (dep,ind,s) -> + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc () + ) ++ + hov 0 ((if dep then str"Elimination for" else str"Case for") + ++ spc() ++ pr_smart_global ind) ++ spc() ++ + hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) | EqualityScheme ind -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() |