diff options
-rw-r--r-- | dev/doc/changes.txt | 5 | ||||
-rw-r--r-- | engine/termops.ml | 22 | ||||
-rw-r--r-- | engine/termops.mli | 4 | ||||
-rw-r--r-- | ide/ide_slave.ml | 9 | ||||
-rw-r--r-- | kernel/context.ml | 2 | ||||
-rw-r--r-- | kernel/context.mli | 2 | ||||
-rw-r--r-- | printing/printer.ml | 22 | ||||
-rw-r--r-- | printing/printer.mli | 2 |
8 files changed, 37 insertions, 31 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 5933649da..f87e76dd1 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -6,6 +6,11 @@ We renamed the following functions: Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr + Printer.pr_var_list_decl -> Printer.pr_compacted_decl + +We renamed the following modules: + + Context.ListNamed -> Context.Compacted The following type aliases where removed diff --git a/engine/termops.ml b/engine/termops.ml index 3f36059dd..1c2d261e5 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -17,7 +17,7 @@ open Environ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -module NamedListDecl = Context.NamedList.Declaration +module CompactedDecl = Context.Compacted.Declaration (* Sorts and sort family *) @@ -986,21 +986,21 @@ let compact_named_context_reverse sign = let compact l decl = match decl, l with | NamedDecl.LocalAssum (i,t), [] -> - [NamedListDecl.LocalAssum ([i],t)] + [CompactedDecl.LocalAssum ([i],t)] | NamedDecl.LocalDef (i,c,t), [] -> - [NamedListDecl.LocalDef ([i],c,t)] - | NamedDecl.LocalAssum (i1,t1), NamedListDecl.LocalAssum (li,t2) :: q -> + [CompactedDecl.LocalDef ([i],c,t)] + | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q -> if Constr.equal t1 t2 - then NamedListDecl.LocalAssum (i1::li, t2) :: q - else NamedListDecl.LocalAssum ([i1],t1) :: NamedListDecl.LocalAssum (li,t2) :: q - | NamedDecl.LocalDef (i1,c1,t1), NamedListDecl.LocalDef (li,c2,t2) :: q -> + then CompactedDecl.LocalAssum (i1::li, t2) :: q + else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q + | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q -> if Constr.equal c1 c2 && Constr.equal t1 t2 - then NamedListDecl.LocalDef (i1::li, c2, t2) :: q - else NamedListDecl.LocalDef ([i1],c1,t1) :: NamedListDecl.LocalDef (li,c2,t2) :: q + then CompactedDecl.LocalDef (i1::li, c2, t2) :: q + else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q | NamedDecl.LocalAssum (i,t), q -> - NamedListDecl.LocalAssum ([i],t) :: q + CompactedDecl.LocalAssum ([i],t) :: q | NamedDecl.LocalDef (i,c,t), q -> - NamedListDecl.LocalDef ([i],c,t) :: q + CompactedDecl.LocalDef ([i],c,t) :: q in Context.Named.fold_inside compact ~init:[] sign diff --git a/engine/termops.mli b/engine/termops.mli index 5d85088f8..bfd902f44 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -238,8 +238,8 @@ val fold_named_context_both_sides : ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> Context.Named.t -> init:'a -> 'a val mem_named_context : Id.t -> Context.Named.t -> bool -val compact_named_context : Context.Named.t -> Context.NamedList.t -val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t +val compact_named_context : Context.Named.t -> Context.Compacted.t +val compact_named_context_reverse : Context.Named.t -> Context.Compacted.t val clear_named_body : Id.t -> env -> env diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 36d676f5d..8ef7a0554 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -15,6 +15,7 @@ open Printer module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +module CompactedDecl = Context.Compacted.Declaration (** Ide_slave : an implementation of [Interface], i.e. mainly an interp function and a rewind function. This specialized loop is triggered @@ -194,12 +195,12 @@ let process_goal sigma g = Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d (env,l) = - let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in - let d' = Context.NamedList.Declaration.to_named_context d in + let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in + let d' = CompactedDecl.to_named_context d in (List.fold_right Environ.push_named d' env, - (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in + (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in let (_env, hyps) = - Context.NamedList.fold process_hyp + Context.Compacted.fold process_hyp (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } diff --git a/kernel/context.ml b/kernel/context.ml index fed6a5feb..47e0a08e5 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -412,7 +412,7 @@ struct List.map_filter filter end -module NamedList = +module Compacted = struct module Declaration = struct diff --git a/kernel/context.mli b/kernel/context.mli index 72fbfb540..366f0ffc1 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -251,7 +251,7 @@ sig val to_instance : t -> Constr.t list end -module NamedList : +module Compacted : sig module Declaration : sig diff --git a/printing/printer.ml b/printing/printer.ml index 5c62c2af0..e3f4ea999 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -24,7 +24,7 @@ open Declarations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -module NamedListDecl = Context.NamedList.Declaration +module CompactedDecl = Context.Compacted.Declaration let emacs_str s = if !Flags.print_emacs then s else "" @@ -252,11 +252,11 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (**********************************************************************) (* Contexts and declarations *) -let pr_var_list_decl env sigma decl = +let pr_compacted_decl env sigma decl = let ids, pbody, typ = match decl with - | NamedListDecl.LocalAssum (ids, typ) -> + | CompactedDecl.LocalAssum (ids, typ) -> ids, mt (), typ - | NamedListDecl.LocalDef (ids,c,typ) -> + | CompactedDecl.LocalDef (ids,c,typ) -> (* Force evaluation *) let pb = pr_lconstr_env env sigma c in let pb = if isCast c then surround pb else pb in @@ -270,11 +270,11 @@ let pr_var_list_decl env sigma decl = let pr_var_decl env sigma decl = let decl = match decl with | NamedDecl.LocalAssum (id, t) -> - NamedListDecl.LocalAssum ([id], t) + CompactedDecl.LocalAssum ([id], t) | NamedDecl.LocalDef (id,c,t) -> - NamedListDecl.LocalDef ([id],c,t) + CompactedDecl.LocalDef ([id],c,t) in - pr_var_list_decl env sigma decl + pr_compacted_decl env sigma decl let pr_rel_decl env sigma decl = let na = RelDecl.get_name decl in @@ -316,9 +316,9 @@ let pr_rel_context_of env sigma = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env sigma = let sign_env = - Context.NamedList.fold + Context.Compacted.fold (fun d pps -> - let pidt = pr_var_list_decl env sigma d in + let pidt = pr_compacted_decl env sigma d in (pps ++ fnl () ++ pidt)) (Termops.compact_named_context (named_context env)) ~init:(mt ()) in @@ -343,12 +343,12 @@ let pr_context_limit n env sigma = else let k = lgsign-n in let _,sign_env = - Context.NamedList.fold + Context.Compacted.fold (fun d (i,pps) -> if i < k then (i+1, (pps ++str ".")) else - let pidt = pr_var_list_decl env sigma d in + let pidt = pr_compacted_decl env sigma d in (i+1, (pps ++ fnl () ++ str (emacs_str "") ++ pidt))) diff --git a/printing/printer.mli b/printing/printer.mli index 695ab33b2..196f7cb54 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -109,7 +109,7 @@ val pr_context_unlimited : env -> evar_map -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds val pr_var_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds -val pr_var_list_decl : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds +val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> std_ppcmds val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds |