aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.gitignore2
-rw-r--r--Makefile.build4
-rw-r--r--dev/doc/changes.txt50
-rw-r--r--engine/evd.mli9
-rw-r--r--engine/namegen.mli13
-rw-r--r--engine/termops.ml29
-rw-r--r--engine/termops.mli77
-rw-r--r--ide/ide_slave.ml4
-rw-r--r--interp/constrextern.mli3
-rw-r--r--interp/constrintern.ml4
-rw-r--r--interp/constrintern.mli5
-rw-r--r--kernel/context.ml356
-rw-r--r--kernel/context.mli243
-rw-r--r--kernel/cooking.ml6
-rw-r--r--kernel/csymtable.ml5
-rw-r--r--kernel/declarations.mli7
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/environ.ml27
-rw-r--r--kernel/environ.mli45
-rw-r--r--kernel/fast_typeops.ml2
-rw-r--r--kernel/indtypes.ml33
-rw-r--r--kernel/indtypes.mli4
-rw-r--r--kernel/inductive.ml15
-rw-r--r--kernel/inductive.mli9
-rw-r--r--kernel/nativecode.ml9
-rw-r--r--kernel/opaqueproof.ml2
-rw-r--r--kernel/opaqueproof.mli2
-rw-r--r--kernel/pre_env.ml17
-rw-r--r--kernel/pre_env.mli13
-rw-r--r--kernel/reduction.ml17
-rw-r--r--kernel/reduction.mli7
-rw-r--r--kernel/term.ml33
-rw-r--r--kernel/term.mli37
-rw-r--r--kernel/term_typing.ml5
-rw-r--r--kernel/typeops.ml7
-rw-r--r--kernel/typeops.mli5
-rw-r--r--kernel/vars.ml11
-rw-r--r--kernel/vars.mli15
-rw-r--r--library/decls.ml3
-rw-r--r--library/global.mli4
-rw-r--r--library/lib.mli8
-rw-r--r--plugins/extraction/extraction.ml1
-rw-r--r--plugins/firstorder/formula.mli3
-rw-r--r--plugins/funind/functional_principles_proofs.ml3
-rw-r--r--plugins/funind/functional_principles_types.ml3
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/merge.ml19
-rw-r--r--pretyping/cases.ml27
-rw-r--r--pretyping/cases.mli9
-rw-r--r--pretyping/constr_matching.ml5
-rw-r--r--pretyping/detyping.ml5
-rw-r--r--pretyping/detyping.mli3
-rw-r--r--pretyping/evarsolve.ml3
-rw-r--r--pretyping/evarutil.ml11
-rw-r--r--pretyping/evarutil.mli7
-rw-r--r--pretyping/find_subterm.mli5
-rw-r--r--pretyping/indrec.ml39
-rw-r--r--pretyping/inductiveops.ml35
-rw-r--r--pretyping/inductiveops.mli19
-rw-r--r--pretyping/pretyping.ml19
-rw-r--r--pretyping/reductionops.ml15
-rw-r--r--pretyping/reductionops.mli7
-rw-r--r--pretyping/retyping.mli3
-rw-r--r--pretyping/typeclasses.ml11
-rw-r--r--pretyping/typeclasses.mli7
-rw-r--r--pretyping/typeclasses_errors.ml3
-rw-r--r--pretyping/typeclasses_errors.mli5
-rw-r--r--pretyping/unification.ml4
-rw-r--r--pretyping/unification.mli2
-rw-r--r--pretyping/vnorm.ml2
-rw-r--r--printing/printer.ml8
-rw-r--r--printing/printer.mli13
-rw-r--r--printing/printmod.ml5
-rw-r--r--proofs/goal.mli2
-rw-r--r--proofs/logic.ml1
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/proofview.mli2
-rw-r--r--proofs/refiner.ml4
-rw-r--r--proofs/refiner.mli3
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--proofs/tacmach.mli11
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/eqschemes.ml71
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/hints.mli3
-rw-r--r--tactics/inv.ml3
-rw-r--r--tactics/leminv.ml9
-rw-r--r--tactics/rewrite.mli2
-rw-r--r--tactics/tactic_matching.mli2
-rw-r--r--tactics/tacticals.ml5
-rw-r--r--tactics/tacticals.mli35
-rw-r--r--tactics/tactics.ml57
-rw-r--r--tactics/tactics.mli37
-rw-r--r--toplevel/assumptions.ml2
-rw-r--r--toplevel/assumptions.mli2
-rw-r--r--toplevel/auto_ind_decl.ml7
-rw-r--r--toplevel/class.ml5
-rw-r--r--toplevel/classes.ml2
-rw-r--r--toplevel/classes.mli5
-rw-r--r--toplevel/command.ml15
-rw-r--r--toplevel/discharge.ml7
-rw-r--r--toplevel/discharge.mli3
-rw-r--r--toplevel/obligations.ml5
-rw-r--r--toplevel/record.ml11
-rw-r--r--toplevel/record.mli7
-rw-r--r--toplevel/vernacentries.ml2
108 files changed, 959 insertions, 829 deletions
diff --git a/.gitignore b/.gitignore
index 0466eac85..5c932ad02 100644
--- a/.gitignore
+++ b/.gitignore
@@ -98,6 +98,8 @@ doc/RecTutorial/RecTutorial.html
doc/RecTutorial/RecTutorial.pdf
doc/RecTutorial/RecTutorial.ps
dev/doc/naming-conventions.pdf
+dev/ocamldoc/*.html
+dev/ocamldoc/*.css
# .mll files
diff --git a/Makefile.build b/Makefile.build
index 9d4f56e2a..bc89d6b99 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -840,7 +840,7 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
mli-doc: $(DOCMLIS:.mli=.cmi)
$(SHOW)'OCAMLDOC -html'
- $(HIDE)$(OCAMLFIND) ocamldoc -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
+ $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-css-style style.css
@@ -862,7 +862,7 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -
$(OCAMLDOC_MLLIBD)
ml-doc:
- $(OCAMLFIND) ocamldoc -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
+ $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
$(OCAMLDOC_MLLIBD)
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2f62be9af..c143afd37 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,54 @@
=========================================
+= CHANGES BETWEEN COQ V8.5 AND CQQ V8.6 =
+=========================================
+
+- The interface of the Context module was changed.
+ Related types and functions were put in separate submodules.
+ The mapping from old identifiers to new identifiers is the following:
+
+ Context.named_declaration ---> Context.Named.Declaration.t
+ Context.named_list_declaration ---> Context.NamedList.Declaration.t
+ Context.rel_declaration ---> Context.Rel.Declaration.t
+ Context.map_named_declaration ---> Context.Named.Declaration.map
+ Context.map_named_list_declaration ---> Context.NamedList.Declaration.map
+ Context.map_rel_declaration ---> Context.Rel.Declaration.map
+ Context.fold_named_declaration ---> Context.Named.Declaration.fold
+ Context.fold_rel_declaration ---> Context.Rel.Declaration.fold
+ Context.exists_named_declaration ---> Context.Named.Declaration.exists
+ Context.exists_rel_declaration ---> Context.Rel.Declaration.exists
+ Context.for_all_named_declaration ---> Context.Named.Declaration.for_all
+ Context.for_all_rel_declaration ---> Context.Rel.Declaration.for_all
+ Context.eq_named_declaration ---> Context.Named.Declaration.equal
+ Context.eq_rel_declaration ---> Context.Rel.Declaration.equal
+ Context.named_context ---> Context.Named.t
+ Context.named_list_context ---> Context.NamedList.t
+ Context.rel_context ---> Context.Rel.t
+ Context.empty_named_context ---> Context.Named.empty
+ Context.add_named_decl ---> Context.Named.add
+ Context.vars_of_named_context ---> Context.Named.to_vars
+ Context.lookup_named ---> Context.Named.lookup
+ Context.named_context_length ---> Context.Named.length
+ Context.named_context_equal ---> Context.Named.equal
+ Context.fold_named_context ---> Context.Named.fold_outside
+ Context.fold_named_list_context ---> Context.NamedList.fold
+ Context.fold_named_context_reverse ---> Context.Named.fold_inside
+ Context.instance_from_named_context ---> Context.Named.to_instance
+ Context.extended_rel_list ---> Context.Rel.to_extended_list
+ Context.extended_rel_vect ---> Context.Rel.to_extended_vect
+ Context.fold_rel_context ---> Context.Rel.fold_outside
+ Context.fold_rel_context_reverse ---> Context.Rel.fold_inside
+ Context.map_rel_context ---> Context.Rel.map
+ Context.map_named_context ---> Context.Named.map
+ Context.iter_rel_context ---> Context.Rel.iter
+ Context.iter_named_context ---> Context.Named.iter
+ Context.empty_rel_context ---> Context.Rel.empty
+ Context.add_rel_decl ---> Context.Rel.add
+ Context.lookup_rel ---> Context.Rel.lookup
+ Context.rel_context_length ---> Context.Rel.length
+ Context.rel_context_nhyps ---> Context.Rel.nhyps
+ Context.rel_context_tags ---> Context.Rel.to_tags
+
+=========================================
= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 =
=========================================
diff --git a/engine/evd.mli b/engine/evd.mli
index 220c693ad..7fef95f17 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -10,7 +10,6 @@ open Util
open Loc
open Names
open Term
-open Context
open Environ
(** {5 Existential variables and unification states}
@@ -105,8 +104,8 @@ type evar_info = {
val make_evar : named_context_val -> types -> evar_info
val evar_concl : evar_info -> constr
-val evar_context : evar_info -> named_context
-val evar_filtered_context : evar_info -> named_context
+val evar_context : evar_info -> Context.Named.t
+val evar_filtered_context : evar_info -> Context.Named.t
val evar_hyps : evar_info -> named_context_val
val evar_filtered_hyps : evar_info -> named_context_val
val evar_body : evar_info -> evar_body
@@ -223,7 +222,7 @@ val existential_opt_value : evar_map -> existential -> constr option
(** Same as {!existential_value} but returns an option instead of raising an
exception. *)
-val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info ->
+val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info ->
'a array -> (Id.t * 'a) list
val instantiate_evar_array : evar_info -> constr -> constr array -> constr
@@ -423,7 +422,7 @@ val evar_list : constr -> existential list
val evars_of_term : constr -> Evar.Set.t
(** including evars in instances of evars *)
-val evars_of_named_context : named_context -> Evar.Set.t
+val evars_of_named_context : Context.Named.t -> Evar.Set.t
val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
diff --git a/engine/namegen.mli b/engine/namegen.mli
index f66bc6d88..617f6e522 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Environ
(*********************************************************************
@@ -39,13 +38,13 @@ val lambda_name : env -> Name.t * types * constr -> constr
val prod_create : env -> types * types -> constr
val lambda_create : env -> types * constr -> constr
-val name_assumption : env -> rel_declaration -> rel_declaration
-val name_context : env -> rel_context -> rel_context
+val name_assumption : env -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
+val name_context : env -> Context.Rel.t -> Context.Rel.t
-val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types
-val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
-val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types
-val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
+val mkProd_or_LetIn_name : env -> types -> Context.Rel.Declaration.t -> types
+val mkLambda_or_LetIn_name : env -> constr -> Context.Rel.Declaration.t -> constr
+val it_mkProd_or_LetIn_name : env -> types -> Context.Rel.t -> types
+val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr
(*********************************************************************
Fresh names *)
diff --git a/engine/termops.ml b/engine/termops.ml
index c10c55220..ce640bacf 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -13,7 +13,6 @@ open Names
open Nameops
open Term
open Vars
-open Context
open Environ
(* Sorts and sort family *)
@@ -700,9 +699,9 @@ let replace_term = replace_term_gen eq_constr
let vars_of_env env =
let s =
- Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s)
+ Context.Named.fold_outside (fun (id,_,_) s -> Id.Set.add id s)
(named_context env) ~init:Id.Set.empty in
- Context.fold_rel_context
+ Context.Rel.fold_outside
(fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s)
(rel_context env) ~init:s
@@ -728,12 +727,12 @@ let lookup_rel_of_name id names =
let empty_names_context = []
let ids_of_rel_context sign =
- Context.fold_rel_context
+ Context.Rel.fold_outside
(fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
sign ~init:[]
let ids_of_named_context sign =
- Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
+ Context.Named.fold_outside (fun (id,_,_) idl -> id::idl) sign ~init:[]
let ids_of_context env =
(ids_of_rel_context (rel_context env))
@@ -788,7 +787,7 @@ let split_app c = match kind_of_term c with
c::(Array.to_list prev), last
| _ -> assert false
-type subst = (rel_context*constr) Evar.Map.t
+type subst = (Context.Rel.t * constr) Evar.Map.t
exception CannotFilter
@@ -825,7 +824,7 @@ let filtering env cv_pb c1 c2 =
in
aux env cv_pb c1 c2; !evm
-let decompose_prod_letin : constr -> int * rel_context * constr =
+let decompose_prod_letin : constr -> int * Context.Rel.t * constr =
let rec prodec_rec i l c = match kind_of_term c with
| Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c
| LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
@@ -861,7 +860,7 @@ let nb_prod_modulo_zeta x =
| _ -> n
in count 0 x
-let align_prod_letin c a : rel_context * constr =
+let align_prod_letin c a : Context.Rel.t * constr =
let (lc,_,_) = decompose_prod_letin c in
let (la,l,a) = decompose_prod_letin a in
if not (la >= lc) then invalid_arg "align_prod_letin";
@@ -899,10 +898,10 @@ let process_rel_context f env =
let sign = named_context_val env in
let rels = rel_context env in
let env0 = reset_with_named_context sign env in
- Context.fold_rel_context f rels ~init:env0
+ Context.Rel.fold_outside f rels ~init:env0
let assums_of_rel_context sign =
- Context.fold_rel_context
+ Context.Rel.fold_outside
(fun (na,c,t) l ->
match c with
Some _ -> l
@@ -912,7 +911,7 @@ let assums_of_rel_context sign =
let map_rel_context_in_env f env sign =
let rec aux env acc = function
| d::sign ->
- aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
+ aux (push_rel d env) (Context.Rel.Declaration.map (f env) d :: acc) sign
| [] ->
acc
in
@@ -920,10 +919,10 @@ let map_rel_context_in_env f env sign =
let map_rel_context_with_binders f sign =
let rec aux k = function
- | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
+ | d::sign -> Context.Rel.Declaration.map (f k) d :: aux (k-1) sign
| [] -> []
in
- aux (rel_context_length sign) sign
+ aux (Context.Rel.length sign) sign
let substl_rel_context l =
map_rel_context_with_binders (fun k -> substnl l (k-1))
@@ -955,7 +954,7 @@ let compact_named_context_reverse sign =
if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
then (i1::l2,c2,t2)::q
else ([i1],c1,t1)::l
- in Context.fold_named_context_reverse compact ~init:[] sign
+ in Context.Named.fold_inside compact ~init:[] sign
let compact_named_context sign = List.rev (compact_named_context_reverse sign)
@@ -976,7 +975,7 @@ let global_vars_set_of_decl env = function
let dependency_closure env sign hyps =
if Id.Set.is_empty hyps then [] else
let (_,lh) =
- Context.fold_named_context_reverse
+ Context.Named.fold_inside
(fun (hs,hl) (x,_,_ as d) ->
if Id.Set.mem x hs then
(Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
diff --git a/engine/termops.mli b/engine/termops.mli
index 6083f1ab5..0fbd1ee82 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -9,7 +9,6 @@
open Pp
open Names
open Term
-open Context
open Environ
(** printers *)
@@ -22,7 +21,7 @@ val set_print_constr : (env -> constr -> std_ppcmds) -> unit
val print_constr : constr -> std_ppcmds
val print_constr_env : env -> constr -> std_ppcmds
val print_named_context : env -> std_ppcmds
-val pr_rel_decl : env -> rel_declaration -> std_ppcmds
+val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
val print_rel_context : env -> std_ppcmds
val print_env : env -> std_ppcmds
@@ -31,7 +30,7 @@ val push_rel_assum : Name.t * types -> env -> env
val push_rels_assum : (Name.t * types) list -> env -> env
val push_named_rec_types : Name.t array * types array * 'a -> env -> env
-val lookup_rel_id : Id.t -> rel_context -> int * constr option * types
+val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types
(** Associates the contents of an identifier in a [rel_context]. Raise
[Not_found] if there is no such identifier. *)
@@ -42,20 +41,20 @@ val rel_vect : int -> int -> constr array
val rel_list : int -> int -> constr list
(** iterators/destructors on terms *)
-val mkProd_or_LetIn : rel_declaration -> types -> types
-val mkProd_wo_LetIn : rel_declaration -> types -> types
+val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
val it_mkProd : types -> (Name.t * types) list -> types
val it_mkLambda : constr -> (Name.t * types) list -> constr
-val it_mkProd_or_LetIn : types -> rel_context -> types
-val it_mkProd_wo_LetIn : types -> rel_context -> types
-val it_mkLambda_or_LetIn : constr -> rel_context -> constr
-val it_mkNamedProd_or_LetIn : types -> named_context -> types
-val it_mkNamedProd_wo_LetIn : types -> named_context -> types
-val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
+val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
+val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types
+val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
+val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types
+val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types
+val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr
(* Ad hoc version reinserting letin, assuming the body is defined in
the context where the letins are expanded *)
-val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr
+val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr
(** {6 Generic iterators on constr} *)
@@ -63,11 +62,11 @@ val map_constr_with_named_binders :
(Name.t -> 'a -> 'a) ->
('a -> constr -> constr) -> 'a -> constr -> constr
val map_constr_with_binders_left_to_right :
- (rel_declaration -> 'a -> 'a) ->
+ (Context.Rel.Declaration.t -> 'a -> 'a) ->
('a -> constr -> constr) ->
'a -> constr -> constr
val map_constr_with_full_binders :
- (rel_declaration -> 'a -> 'a) ->
+ (Context.Rel.Declaration.t -> 'a -> 'a) ->
('a -> constr -> constr) -> 'a -> constr -> constr
(** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
@@ -81,11 +80,11 @@ val fold_constr_with_binders :
('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
val fold_constr_with_full_binders :
- (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
+ (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
'a -> 'b -> constr -> 'b
val iter_constr_with_full_binders :
- (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
+ (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
constr -> unit
(**********************************************************************)
@@ -110,7 +109,7 @@ val dependent : constr -> constr -> bool
val dependent_no_evar : constr -> constr -> bool
val dependent_univs : constr -> constr -> bool
val dependent_univs_no_evar : constr -> constr -> bool
-val dependent_in_decl : constr -> named_declaration -> bool
+val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool
val count_occurrences : constr -> constr -> int
val collect_metas : constr -> int list
val collect_vars : constr -> Id.Set.t (** for visible vars only *)
@@ -164,11 +163,11 @@ exception CannotFilter
(context,term), or raises [CannotFilter].
Warning: Outer-kernel sort subtyping are taken into account: c1 has
to be smaller than c2 wrt. sorts. *)
-type subst = (rel_context*constr) Evar.Map.t
-val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
+type subst = (Context.Rel.t * constr) Evar.Map.t
+val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
-val decompose_prod_letin : constr -> int * rel_context * constr
-val align_prod_letin : constr -> constr -> rel_context * constr
+val decompose_prod_letin : constr -> int * Context.Rel.t * constr
+val align_prod_letin : constr -> constr -> Context.Rel.t * constr
(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
gives {% $ %}n{% $ %} (casts are ignored) *)
@@ -197,51 +196,51 @@ val add_name : Name.t -> names_context -> names_context
val lookup_name_of_rel : int -> names_context -> Name.t
val lookup_rel_of_name : Id.t -> names_context -> int
val empty_names_context : names_context
-val ids_of_rel_context : rel_context -> Id.t list
-val ids_of_named_context : named_context -> Id.t list
+val ids_of_rel_context : Context.Rel.t -> Id.t list
+val ids_of_named_context : Context.Named.t -> Id.t list
val ids_of_context : env -> Id.t list
val names_of_rel_context : env -> names_context
(* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has
[n] hypotheses, excluding local definitions, and [Γ₁], if not empty,
starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *)
-val context_chop : int -> rel_context -> rel_context * rel_context
+val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t
(* [env_rel_context_chop n env] extracts out the [n] top declarations
of the rel_context part of [env], counting both local definitions and
hypotheses *)
-val env_rel_context_chop : int -> env -> env * rel_context
+val env_rel_context_chop : int -> env -> env * Context.Rel.t
(** Set of local names *)
val vars_of_env: env -> Id.Set.t
val add_vname : Id.Set.t -> Name.t -> Id.Set.t
(** other signature iterators *)
-val process_rel_context : (rel_declaration -> env -> env) -> env -> env
-val assums_of_rel_context : rel_context -> (Name.t * constr) list
-val lift_rel_context : int -> rel_context -> rel_context
-val substl_rel_context : constr list -> rel_context -> rel_context
-val smash_rel_context : rel_context -> rel_context (** expand lets in context *)
+val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env
+val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list
+val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t
+val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t
+val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *)
val map_rel_context_in_env :
- (env -> constr -> constr) -> env -> rel_context -> rel_context
+ (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t
val map_rel_context_with_binders :
- (int -> constr -> constr) -> rel_context -> rel_context
+ (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t
val fold_named_context_both_sides :
- ('a -> named_declaration -> named_declaration list -> 'a) ->
- named_context -> init:'a -> 'a
-val mem_named_context : Id.t -> named_context -> bool
-val compact_named_context : named_context -> named_list_context
-val compact_named_context_reverse : named_context -> named_list_context
+ ('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 clear_named_body : Id.t -> env -> env
val global_vars : env -> constr -> Id.t list
-val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t
+val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t
(** Gives an ordered list of hypotheses, closed by dependencies,
containing a given set *)
-val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list
+val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list
(** Test if an identifier is the basename of a global reference *)
val is_section_variable : Id.t -> bool
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index a6c42b28c..d8b8bd461 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -187,12 +187,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.map_named_list_declaration (Reductionops.nf_evar sigma) d in
+ let d = Context.NamedList.Declaration.map (Reductionops.nf_evar sigma) d in
let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
(List.fold_right Environ.push_named d' env,
(Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
let (_env, hyps) =
- Context.fold_named_list_context process_hyp
+ Context.NamedList.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/interp/constrextern.mli b/interp/constrextern.mli
index b797e455c..ff8ca0b7c 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Termops
open Environ
open Libnames
@@ -42,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> sorts -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
- rel_context -> local_binder list
+ Context.Rel.t -> local_binder list
(** Printing options *)
val print_implicits : bool ref
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f9de8c466..68bc0b109 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -101,7 +101,7 @@ let global_reference id =
let construct_reference ctx id =
try
- Term.mkVar (let _ = Context.lookup_named id ctx in id)
+ Term.mkVar (let _ = Context.Named.lookup id ctx in id)
with Not_found ->
global_reference id
@@ -685,7 +685,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
str "variable " ++ pr_id id ++ str " should be bound to a term.")
else
(* Is [id] a goal or section variable *)
- let _ = Context.lookup_named id namedctx in
+ let _ = Context.Named.lookup id namedctx in
try
(* [id] a section variable *)
(* Redundant: could be done in intern_qualid *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b671c9881..c851fbb36 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Evd
open Environ
open Libnames
@@ -161,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
val interp_context_evars :
?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
env -> evar_map ref -> local_binder list ->
- internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+ internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits)
(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
(* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
@@ -178,7 +177,7 @@ val interp_context_evars :
val locate_reference : Libnames.qualid -> Globnames.global_reference
val is_global : Id.t -> bool
-val construct_reference : named_context -> Id.t -> constr
+val construct_reference : Context.Named.t -> Id.t -> constr
val global_reference : Id.t -> constr
val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
diff --git a/kernel/context.ml b/kernel/context.ml
index 5923048fa..372f16a8d 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -15,137 +15,233 @@
(* This file defines types and combinators regarding indexes-based and
names-based contexts *)
-open Util
-open Names
-
-(***************************************************************************)
-(* Type of assumptions *)
-(***************************************************************************)
-
-type named_declaration = Id.t * Constr.t option * Constr.t
-type named_list_declaration = Id.t list * Constr.t option * Constr.t
-type rel_declaration = Name.t * Constr.t option * Constr.t
-
-let map_named_declaration_skel f (id, (v : Constr.t option), ty) =
- (id, Option.map f v, f ty)
-let map_named_list_declaration = map_named_declaration_skel
-let map_named_declaration = map_named_declaration_skel
-
-let map_rel_declaration = map_named_declaration
-
-let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
-let fold_rel_declaration = fold_named_declaration
-
-let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty
-let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty
-
-let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
-let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
-
-let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
- Id.equal i1 i2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-
-let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
- Name.equal n1 n2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-
-(***************************************************************************)
-(* Type of local contexts (telescopes) *)
-(***************************************************************************)
-
-(*s Signatures of ordered optionally named variables, intended to be
- accessed by de Bruijn indices (to represent bound variables) *)
-
-type rel_context = rel_declaration list
-
-let empty_rel_context = []
-
-let add_rel_decl d ctxt = d::ctxt
-
-let rec lookup_rel n sign =
- match n, sign with
- | 1, decl :: _ -> decl
- | n, _ :: sign -> lookup_rel (n-1) sign
- | _, [] -> raise Not_found
-
-let rel_context_length = List.length
+(** The modules defined below represent a {e local context}
+ as defined by Chapter 4 in the Reference Manual:
-let rel_context_nhyps hyps =
- let rec nhyps acc = function
- | [] -> acc
- | (_,None,_)::hyps -> nhyps (1+acc) hyps
- | (_,Some _,_)::hyps -> nhyps acc hyps in
- nhyps 0 hyps
+ A {e local context} is an ordered list of of {e local declarations}
+ of names that we call {e variables}.
-let rel_context_tags ctx =
- let rec aux l = function
- | [] -> l
- | (_,Some _,_)::ctx -> aux (true::l) ctx
- | (_,None,_)::ctx -> aux (false::l) ctx
- in aux [] ctx
+ A {e local declaration} of some variable can be either:
+ - a {e local assumption}, or
+ - a {e local definition}.
+*)
-(*s Signatures of named hypotheses. Used for section variables and
- goal assumptions. *)
-
-type named_context = named_declaration list
-type named_list_context = named_list_declaration list
-
-let empty_named_context = []
-
-let add_named_decl d sign = d::sign
-
-let rec lookup_named id = function
- | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
- | _ :: sign -> lookup_named id sign
- | [] -> raise Not_found
-
-let named_context_length = List.length
-let named_context_equal = List.equal eq_named_declaration
-
-let vars_of_named_context ctx =
- List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty ctx
-
-let instance_from_named_context sign =
- let filter = function
- | (id, None, _) -> Some (Constr.mkVar id)
- | (_, Some _, _) -> None
- in
- List.map_filter filter sign
-
-(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
- with n = |Δ| and with the local definitions of [Γ] skipped in
- [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
-
-let extended_rel_list n hyps =
- let rec reln l p = function
- | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
- | (_, Some _, _) :: hyps -> reln l (p+1) hyps
- | [] -> l
- in
- reln [] 1 hyps
-
-let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
-
-let fold_named_context f l ~init = List.fold_right f l init
-let fold_named_list_context f l ~init = List.fold_right f l init
-let fold_named_context_reverse f ~init l = List.fold_left f init l
-
-(*s Signatures of ordered section variables *)
-type section_context = named_context
-
-let fold_rel_context f l ~init:x = List.fold_right f l x
-let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
-
-let map_context f l =
- let map_decl (n, body_o, typ as decl) =
- let body_o' = Option.smartmap f body_o in
- let typ' = f typ in
- if body_o' == body_o && typ' == typ then decl else
- (n, body_o', typ')
- in
- List.smartmap map_decl l
-
-let map_rel_context = map_context
-let map_named_context = map_context
+open Util
+open Names
-let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+(** Representation of contexts that can capture anonymous as well as non-anonymous variables.
+ Individual declarations are then designated by de Bruijn indexes. *)
+module Rel =
+ struct
+ (** Representation of {e local declarations}.
+
+ [(name, None, typ)] represents a {e local assumption}.
+ In the Reference Manual we denote them as [(name:typ)].
+
+ [(name, Some value, typ)] represents a {e local definition}.
+ In the Reference Manual we denote them as [(name := value : typ)].
+ *)
+ module Declaration =
+ struct
+ type t = Name.t * Constr.t option * Constr.t
+
+ (** Map all terms in a given declaration. *)
+ let map f (n, v, ty) = (n, Option.map f v, f ty)
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
+
+ (** Check whether any term in a given declaration satisfies a given predicate. *)
+ let exists f (_, v, ty) = Option.cata f false v || f ty
+
+ (** Check whether all terms in a given declaration satisfy a given predicate. *)
+ let for_all f (_, v, ty) = Option.cata f true v && f ty
+
+ (** Check whether the two given declarations are equal. *)
+ let equal (n1, v1, ty1) (n2, v2, ty2) =
+ Name.equal n1 n2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
+ end
+
+ (** Rel-context is represented as a list of declarations.
+ Inner-most declarations are at the beginning of the list.
+ Outer-most declarations are at the end of the list. *)
+ type t = Declaration.t list
+
+ (** empty rel-context *)
+ let empty = []
+
+ (** Return a new rel-context enriched by with a given inner-most declaration. *)
+ let add d ctx = d :: ctx
+
+ (** Return a declaration designated by a given de Bruijn index.
+ @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *)
+ let rec lookup n ctx =
+ match n, ctx with
+ | 1, decl :: _ -> decl
+ | n, _ :: sign -> lookup (n-1) sign
+ | _, [] -> raise Not_found
+
+ (** Map all terms in a given rel-context. *)
+ let map f =
+ let map_decl (n, body_o, typ as decl) =
+ let body_o' = Option.smartmap f body_o in
+ let typ' = f typ in
+ if body_o' == body_o && typ' == typ then decl else
+ (n, body_o', typ')
+ in
+ List.smartmap map_decl
+
+ (** Reduce all terms in a given rel-context to a single value.
+ Innermost declarations are processed first. *)
+ let fold_inside f ~init = List.fold_left f init
+
+ (** Reduce all terms in a given rel-context to a single value.
+ Outermost declarations are processed first. *)
+ let fold_outside f l ~init = List.fold_right f l init
+
+ (** Perform a given action on every declaration in a given rel-context. *)
+ let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+
+ (** Return the number of {e local declarations} in a given context. *)
+ let length = List.length
+
+ (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+ with n = |Δ| and with the local definitions of [Γ] skipped in
+ [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+ let nhyps =
+ let rec nhyps acc = function
+ | [] -> acc
+ | (_,None,_)::hyps -> nhyps (1+acc) hyps
+ | (_,Some _,_)::hyps -> nhyps acc hyps in
+ nhyps 0
+
+ (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
+ and each {e local definition} is mapped to [false]. *)
+ let to_tags =
+ let rec aux l = function
+ | [] -> l
+ | (_,Some _,_)::ctx -> aux (true::l) ctx
+ | (_,None,_)::ctx -> aux (false::l) ctx
+ in aux []
+
+ (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+ with n = |Δ| and with the {e local definitions} of [Γ] skipped in
+ [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+ let to_extended_list n =
+ let rec reln l p = function
+ | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
+ | (_, Some _, _) :: hyps -> reln l (p+1) hyps
+ | [] -> l
+ in
+ reln [] 1
+
+ (** [extended_vect n Γ] does the same, returning instead an array. *)
+ let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps)
+ end
+
+(** This module represents contexts that can capture non-anonymous variables.
+ Individual declarations are then designated by the identifiers they bind. *)
+module Named =
+ struct
+ (** Representation of {e local declarations}.
+
+ [(id, None, typ)] represents a {e local assumption}.
+ In the Reference Manual we denote them as [(name:typ)].
+
+ [(id, Some value, typ)] represents a {e local definition}.
+ In the Reference Manual we denote them as [(name := value : typ)].
+ *)
+ module Declaration =
+ struct
+ (** Named-context is represented as a list of declarations.
+ Inner-most declarations are at the beginning of the list.
+ Outer-most declarations are at the end of the list. *)
+ type t = Id.t * Constr.t option * Constr.t
+
+ (** Map all terms in a given declaration. *)
+ let map = Rel.Declaration.map
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
+
+ (** Check whether any term in a given declaration satisfies a given predicate. *)
+ let exists f (_, v, ty) = Option.cata f false v || f ty
+
+ (** Check whether all terms in a given declaration satisfy a given predicate. *)
+ let for_all f (_, v, ty) = Option.cata f true v && f ty
+
+ (** Check whether the two given declarations are equal. *)
+ let equal (i1, v1, ty1) (i2, v2, ty2) =
+ Id.equal i1 i2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
+ end
+
+ type t = Declaration.t list
+
+ (** empty named-context *)
+ let empty = []
+
+ (** empty named-context *)
+ let add d ctx = d :: ctx
+
+ (** Return a declaration designated by a given de Bruijn index.
+ @raise Not_found if the designated identifier is not present in the designated named-context. *)
+ let rec lookup id = function
+ | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
+ | _ :: sign -> lookup id sign
+ | [] -> raise Not_found
+
+ (** Map all terms in a given named-context. *)
+ let map f =
+ let map_decl (n, body_o, typ as decl) =
+ let body_o' = Option.smartmap f body_o in
+ let typ' = f typ in
+ if body_o' == body_o && typ' == typ then decl else
+ (n, body_o', typ')
+ in
+ List.smartmap map_decl
+
+ (** Reduce all terms in a given named-context to a single value.
+ Innermost declarations are processed first. *)
+ let fold_inside f ~init = List.fold_left f init
+
+ (** Reduce all terms in a given named-context to a single value.
+ Outermost declarations are processed first. *)
+ let fold_outside f l ~init = List.fold_right f l init
+
+ (** Perform a given action on every declaration in a given named-context. *)
+ let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+
+ (** Return the number of {e local declarations} in a given named-context. *)
+ let length = List.length
+
+ (** Check whether given two named-contexts are equal. *)
+ let equal = List.equal Declaration.equal
+
+ (** Return the set of all identifiers bound in a given named-context. *)
+ let to_vars =
+ List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty
+
+ (** [instance_from_named_context Ω] builds an instance [args] such
+ that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+ definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
+ gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
+ let to_instance =
+ let filter = function
+ | (id, None, _) -> Some (Constr.mkVar id)
+ | (_, Some _, _) -> None
+ in
+ List.map_filter filter
+ end
+
+module NamedList =
+ struct
+ module Declaration =
+ struct
+ type t = Id.t list * Constr.t option * Constr.t
+ let map = Named.Declaration.map
+ end
+ type t = Declaration.t list
+ let fold f l ~init = List.fold_right f l init
+ end
+
+type section_context = Named.t
diff --git a/kernel/context.mli b/kernel/context.mli
index 735467747..0db82beb5 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -6,131 +6,186 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** The modules defined below represent a {e local context}
+ as defined by Chapter 4 in the Reference Manual:
+
+ A {e local context} is an ordered list of of {e local declarations}
+ of names that we call {e variables}.
+
+ A {e local declaration} of some variable can be either:
+ - a {e local assumption}, or
+ - a {e local definition}.
+
+ {e Local assumptions} are denoted in the Reference Manual as [(name : typ)] and
+ {e local definitions} are there denoted as [(name := value : typ)].
+*)
+
open Names
-(** TODO: cleanup *)
+(** Representation of contexts that can capture anonymous as well as non-anonymous variables.
+ Individual declarations are then designated by de Bruijn indexes. *)
+module Rel :
+sig
+ (** Representation of {e local declarations}.
+
+ [(name, None, typ)] represents a {e local assumption}.
+
+ [(name, Some value, typ)] represents a {e local definition}.
+ *)
+ module Declaration :
+ sig
+ type t = Name.t * Constr.t option * Constr.t
+
+ (** Map all terms in a given declaration. *)
+ val map : (Constr.t -> Constr.t) -> t -> t
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+ (** Check whether any term in a given declaration satisfies a given predicate. *)
+ val exists : (Constr.t -> bool) -> t -> bool
+
+ (** Check whether all terms in a given declaration satisfy a given predicate. *)
+ val for_all : (Constr.t -> bool) -> t -> bool
+
+ (** Check whether the two given declarations are equal. *)
+ val equal : t -> t -> bool
+ end
+
+ (** Rel-context is represented as a list of declarations.
+ Inner-most declarations are at the beginning of the list.
+ Outer-most declarations are at the end of the list. *)
+ type t = Declaration.t list
+
+ (** empty rel-context *)
+ val empty : t
+
+ (** Return a new rel-context enriched by with a given inner-most declaration. *)
+ val add : Declaration.t -> t -> t
+
+ (** Return a declaration designated by a given de Bruijn index.
+ @raise Not_found if the designated de Bruijn index outside the range. *)
+ val lookup : int -> t -> Declaration.t
+
+ (** Map all terms in a given rel-context. *)
+ val map : (Constr.t -> Constr.t) -> t -> t
-(** {6 Declarations} *)
-(** A {e declaration} has the form [(name,body,type)]. It is either an
- {e assumption} if [body=None] or a {e definition} if
- [body=Some actualbody]. It is referred by {e name} if [na] is an
- identifier or by {e relative index} if [na] is not an identifier
- (in the latter case, [na] is of type [name] but just for printing
- purpose) *)
+ (** Reduce all terms in a given rel-context to a single value.
+ Innermost declarations are processed first. *)
+ val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a
-type named_declaration = Id.t * Constr.t option * Constr.t
-type named_list_declaration = Id.t list * Constr.t option * Constr.t
-type rel_declaration = Name.t * Constr.t option * Constr.t
+ (** Reduce all terms in a given rel-context to a single value.
+ Outermost declarations are processed first. *)
+ val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
-val map_named_declaration :
- (Constr.t -> Constr.t) -> named_declaration -> named_declaration
-val map_named_list_declaration :
- (Constr.t -> Constr.t) -> named_list_declaration -> named_list_declaration
-val map_rel_declaration :
- (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration
+ (** Perform a given action on every declaration in a given rel-context. *)
+ val iter : (Constr.t -> unit) -> t -> unit
-val fold_named_declaration :
- (Constr.t -> 'a -> 'a) -> named_declaration -> 'a -> 'a
-val fold_rel_declaration :
- (Constr.t -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
+ (** Return the number of {e local declarations} in a given context. *)
+ val length : t -> int
-val exists_named_declaration :
- (Constr.t -> bool) -> named_declaration -> bool
-val exists_rel_declaration :
- (Constr.t -> bool) -> rel_declaration -> bool
+ (** Return the number of {e local assumptions} in a given rel-context. *)
+ val nhyps : t -> int
-val for_all_named_declaration :
- (Constr.t -> bool) -> named_declaration -> bool
-val for_all_rel_declaration :
- (Constr.t -> bool) -> rel_declaration -> bool
+ (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
+ and each {e local definition} is mapped to [false]. *)
+ val to_tags : t -> bool list
-val eq_named_declaration :
- named_declaration -> named_declaration -> bool
+ (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+ with n = |Δ| and with the {e local definitions} of [Γ] skipped in
+ [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+ val to_extended_list : int -> t -> Constr.t list
-val eq_rel_declaration :
- rel_declaration -> rel_declaration -> bool
+ (** [extended_vect n Γ] does the same, returning instead an array. *)
+ val to_extended_vect : int -> t -> Constr.t array
+end
-(** {6 Signatures of ordered named declarations } *)
+(** This module represents contexts that can capture non-anonymous variables.
+ Individual declarations are then designated by the identifiers they bind. *)
+module Named :
+sig
+ (** Representation of {e local declarations}.
-type named_context = named_declaration list
-type section_context = named_context
-type named_list_context = named_list_declaration list
-type rel_context = rel_declaration list
-(** In [rel_context], more recent declaration is on top *)
+ [(id, None, typ)] represents a {e local assumption}.
-val empty_named_context : named_context
-val add_named_decl : named_declaration -> named_context -> named_context
-val vars_of_named_context : named_context -> Id.Set.t
+ [(id, Some value, typ)] represents a {e local definition}.
+ *)
+ module Declaration :
+ sig
+ type t = Id.t * Constr.t option * Constr.t
-val lookup_named : Id.t -> named_context -> named_declaration
+ (** Map all terms in a given declaration. *)
+ val map : (Constr.t -> Constr.t) -> t -> t
-(** number of declarations *)
-val named_context_length : named_context -> int
+ (** Reduce all terms in a given declaration to a single value. *)
+ val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
-(** named context equality *)
-val named_context_equal : named_context -> named_context -> bool
+ (** Check whether any term in a given declaration satisfies a given predicate. *)
+ val exists : (Constr.t -> bool) -> t -> bool
-(** {6 Recurrence on [named_context]: older declarations processed first } *)
-val fold_named_context :
- (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
+ (** Check whether all terms in a given declaration satisfy a given predicate. *)
+ val for_all : (Constr.t -> bool) -> t -> bool
-val fold_named_list_context :
- (named_list_declaration -> 'a -> 'a) -> named_list_context -> init:'a -> 'a
+ (** Check whether the two given declarations are equal. *)
+ val equal : t -> t -> bool
+ end
-(** newer declarations first *)
-val fold_named_context_reverse :
- ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
+ (** Rel-context is represented as a list of declarations.
+ Inner-most declarations are at the beginning of the list.
+ Outer-most declarations are at the end of the list. *)
+ type t = Declaration.t list
-(** {6 Section-related auxiliary functions } *)
+ (** empty named-context *)
+ val empty : t
-(** [instance_from_named_context Ω] builds an instance [args] such
- that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
- definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
- gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
-val instance_from_named_context : named_context -> Constr.t list
+ (** Return a new rel-context enriched by with a given inner-most declaration. *)
+ val add : Declaration.t -> t -> t
-(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
- with n = |Δ| and with the local definitions of [Γ] skipped in
- [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
-val extended_rel_list : int -> rel_context -> Constr.t list
+ (** Return a declaration designated by an identifier of the variable bound in that declaration.
+ @raise Not_found if the designated identifier is not bound in a given named-context. *)
+ val lookup : Id.t -> t -> Declaration.t
-(** [extended_rel_vect n Γ] does the same, returning instead an array. *)
-val extended_rel_vect : int -> rel_context -> Constr.t array
+ (** Map all terms in a given named-context. *)
+ val map : (Constr.t -> Constr.t) -> t -> t
-(** {6 ... } *)
-(** Signatures of ordered optionally named variables, intended to be
- accessed by de Bruijn indices *)
+ (** Reduce all terms in a given named-context to a single value.
+ Innermost declarations are processed first. *)
+ val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a
-(** {6 Recurrence on [rel_context]: older declarations processed first } *)
-val fold_rel_context :
- (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+ (** Reduce all terms in a given named-context to a single value.
+ Outermost declarations are processed first. *)
+ val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
-(** newer declarations first *)
-val fold_rel_context_reverse :
- ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
+ (** Perform a given action on every declaration in a given named-context. *)
+ val iter : (Constr.t -> unit) -> t -> unit
-(** {6 Map function of [rel_context] } *)
-val map_rel_context : (Constr.t -> Constr.t) -> rel_context -> rel_context
+ (** Return the number of {e local declarations} in a given named-context. *)
+ val length : t -> int
-(** {6 Map function of [named_context] } *)
-val map_named_context : (Constr.t -> Constr.t) -> named_context -> named_context
+ (** Check whether given two named-contexts are equal. *)
+ val equal : t -> t -> bool
-(** {6 Map function of [rel_context] } *)
-val iter_rel_context : (Constr.t -> unit) -> rel_context -> unit
+ (** Return the set of all identifiers bound in a given named-context. *)
+ val to_vars : t -> Id.Set.t
-(** {6 Map function of [named_context] } *)
-val iter_named_context : (Constr.t -> unit) -> named_context -> unit
+ (** [instance_from_named_context Ω] builds an instance [args] such
+ that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+ definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
+ gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
+ val to_instance : t -> Constr.t list
+end
-(** {6 Contexts of declarations referred to by de Bruijn indices } *)
+module NamedList :
+sig
+ module Declaration :
+ sig
+ type t = Id.t list * Constr.t option * Constr.t
+ val map : (Constr.t -> Constr.t) -> t -> t
+ end
-val empty_rel_context : rel_context
-val add_rel_decl : rel_declaration -> rel_context -> rel_context
+ type t = Declaration.t list
-val lookup_rel : int -> rel_context -> rel_declaration
-(** Size of the [rel_context] including LetIns *)
-val rel_context_length : rel_context -> int
-(** Size of the [rel_context] without LetIns *)
-val rel_context_nhyps : rel_context -> int
-(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
-val rel_context_tags : rel_context -> bool list
+ val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
+end
+type section_context = Named.t
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index be71bd7b4..1302e71c9 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -173,7 +173,7 @@ let expmod_constr_subst cache modlist subst c =
let cook_constr { Opaqueproof.modlist ; abstract } c =
let cache = RefTable.create 13 in
let expmod = expmod_constr_subst cache modlist (pi2 abstract) in
- let hyps = Context.map_named_context expmod (pi1 abstract) in
+ let hyps = Context.Named.map expmod (pi1 abstract) in
abstract_constant_body (expmod c) hyps
let lift_univs cb subst =
@@ -195,13 +195,13 @@ let cook_constant env { from = cb; info } =
let abstract, usubst, abs_ctx = abstract in
let usubst, univs = lift_univs cb usubst in
let expmod = expmod_constr_subst cache modlist usubst in
- let hyps = Context.map_named_context expmod abstract in
+ let hyps = Context.Named.map expmod abstract in
let body = on_body modlist (hyps, usubst, abs_ctx)
(fun c -> abstract_constant_body (expmod c) hyps)
cb.const_body
in
let const_hyps =
- Context.fold_named_context (fun (h,_,_) hyps ->
+ Context.Named.fold_outside (fun (h,_,_) hyps ->
List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps)
hyps ~init:cb.const_hyps in
let typ = match cb.const_type with
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index aa9ef66fe..2067eb899 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -15,7 +15,6 @@
open Util
open Names
open Term
-open Context
open Vm
open Cemitcodes
open Cbytecodes
@@ -190,7 +189,7 @@ and slot_for_fv env fv =
let nv = Pre_env.lookup_named_val id env in
begin match force_lazy_val nv with
| None ->
- let _, b, _ = Context.lookup_named id env.env_named_context in
+ let _, b, _ = Context.Named.lookup id env.env_named_context in
fill_fv_cache nv id val_of_named idfun b
| Some (v, _) -> v
end
@@ -198,7 +197,7 @@ and slot_for_fv env fv =
let rv = Pre_env.lookup_rel_val i env in
begin match force_lazy_val rv with
| None ->
- let _, b, _ = lookup_rel i env.env_rel_context in
+ let _, b, _ = Context.Rel.lookup i env.env_rel_context in
fill_fv_cache rv i val_of_rel env_of_rel b
| Some (v, _) -> v
end
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 0b8272b43..ebf12bd60 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
(** This module defines the internal representation of global
declarations. This includes global constants/axioms, mutual
@@ -38,7 +37,7 @@ type ('a, 'b) declaration_arity =
| RegularArity of 'a
| TemplateArity of 'b
-type constant_type = (types, rel_context * template_arity) declaration_arity
+type constant_type = (types, Context.Rel.t * template_arity) declaration_arity
(** Inlining level of parameters at functor applications.
None means no inlining *)
@@ -117,7 +116,7 @@ type one_inductive_body = {
mind_typename : Id.t; (** Name of the type: [Ii] *)
- mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
+ mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
mind_arity : inductive_arity; (** Arity sort and original user arity *)
@@ -171,7 +170,7 @@ type mutual_inductive_body = {
mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *)
- mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *)
+ mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *)
mind_polymorphic : bool; (** Is it polymorphic or not *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 803df7827..cc11b98c3 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -254,7 +254,7 @@ let subst_mind_body sub mib =
mind_nparams = mib.mind_nparams;
mind_nparams_rec = mib.mind_nparams_rec;
mind_params_ctxt =
- Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
+ Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_polymorphic = mib.mind_polymorphic;
mind_universes = mib.mind_universes;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 09fe64d77..da540bb05 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -24,7 +24,6 @@ open Errors
open Util
open Names
open Term
-open Context
open Vars
open Declarations
open Pre_env
@@ -70,7 +69,7 @@ let empty_context env =
(* Rel context *)
let lookup_rel n env =
- lookup_rel n env.env_rel_context
+ Context.Rel.lookup n env.env_rel_context
let evaluable_rel n env =
match lookup_rel n env with
@@ -81,7 +80,7 @@ let nb_rel env = env.env_nb_rel
let push_rel = push_rel
-let push_rel_context ctxt x = Context.fold_rel_context push_rel ctxt ~init:x
+let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x
let push_rec_types (lna,typarray,_) env =
let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
@@ -120,7 +119,7 @@ let map_named_val f (ctxt,ctxtv) =
in
(map ctxt, ctxtv)
-let empty_named_context = empty_named_context
+let empty_named_context = Context.Named.empty
let push_named = push_named
let push_named_context = List.fold_right push_named
@@ -130,11 +129,11 @@ let val_of_named_context ctxt =
List.fold_right push_named_context_val ctxt empty_named_context_val
-let lookup_named id env = Context.lookup_named id env.env_named_context
-let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt
+let lookup_named id env = Context.Named.lookup id env.env_named_context
+let lookup_named_val id (ctxt,_) = Context.Named.lookup id ctxt
let eq_named_context_val c1 c2 =
- c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2)
+ c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2)
(* A local const is evaluable if it is defined *)
@@ -153,7 +152,7 @@ let reset_with_named_context (ctxt,ctxtv) env =
{ env with
env_named_context = ctxt;
env_named_vals = ctxtv;
- env_rel_context = empty_rel_context;
+ env_rel_context = Context.Rel.empty;
env_rel_val = [];
env_nb_rel = 0 }
@@ -176,7 +175,7 @@ let fold_named_context f env ~init =
in fold_right env
let fold_named_context_reverse f ~init env =
- Context.fold_named_context_reverse f ~init:init (named_context env)
+ Context.Named.fold_inside f ~init:init (named_context env)
(* Universe constraints *)
@@ -389,11 +388,11 @@ let add_mind kn mib env =
let lookup_constant_variables c env =
let cmap = lookup_constant c env in
- Context.vars_of_named_context cmap.const_hyps
+ Context.Named.to_vars cmap.const_hyps
let lookup_inductive_variables (kn,i) env =
let mis = lookup_mind kn env in
- Context.vars_of_named_context mis.mind_hyps
+ Context.Named.to_vars mis.mind_hyps
let lookup_constructor_variables (ind,_) env =
lookup_inductive_variables ind env
@@ -427,7 +426,7 @@ let global_vars_set env constr =
contained in the types of the needed variables. *)
let really_needed env needed =
- Context.fold_named_context_reverse
+ Context.Named.fold_inside
(fun need (id,copt,t) ->
if Id.Set.mem id need then
let globc =
@@ -443,9 +442,9 @@ let really_needed env needed =
let keep_hyps env needed =
let really_needed = really_needed env needed in
- Context.fold_named_context
+ Context.Named.fold_outside
(fun (id,_,_ as d) nsign ->
- if Id.Set.mem id really_needed then add_named_decl d nsign
+ if Id.Set.mem id really_needed then Context.Named.add d nsign
else nsign)
(named_context env)
~init:empty_named_context
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 2eab32e72..f3fe4d6ae 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Declarations
open Univ
@@ -42,8 +41,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
val empty_env : env
val universes : env -> UGraph.t
-val rel_context : env -> rel_context
-val named_context : env -> named_context
+val rel_context : env -> Context.Rel.t
+val named_context : env -> Context.Named.t
val named_context_val : env -> named_context_val
val opaque_tables : env -> Opaqueproof.opaquetab
@@ -60,25 +59,25 @@ val empty_context : env -> bool
(** {5 Context of de Bruijn variables ([rel_context]) } *)
val nb_rel : env -> int
-val push_rel : rel_declaration -> env -> env
-val push_rel_context : rel_context -> env -> env
+val push_rel : Context.Rel.Declaration.t -> env -> env
+val push_rel_context : Context.Rel.t -> env -> env
val push_rec_types : rec_declaration -> env -> env
(** Looks up in the context of local vars referred by indice ([rel_context])
raises [Not_found] if the index points out of the context *)
-val lookup_rel : int -> env -> rel_declaration
+val lookup_rel : int -> env -> Context.Rel.Declaration.t
val evaluable_rel : int -> env -> bool
(** {6 Recurrence on [rel_context] } *)
val fold_rel_context :
- (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+ (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
(** {5 Context of variables (section variables and goal assumptions) } *)
-val named_context_of_val : named_context_val -> named_context
+val named_context_of_val : named_context_val -> Context.Named.t
val named_vals_of_val : named_context_val -> Pre_env.named_vals
-val val_of_named_context : named_context -> named_context_val
+val val_of_named_context : Context.Named.t -> named_context_val
val empty_named_context_val : named_context_val
@@ -88,18 +87,18 @@ val empty_named_context_val : named_context_val
val map_named_val :
(constr -> constr) -> named_context_val -> named_context_val
-val push_named : named_declaration -> env -> env
-val push_named_context : named_context -> env -> env
+val push_named : Context.Named.Declaration.t -> env -> env
+val push_named_context : Context.Named.t -> env -> env
val push_named_context_val :
- named_declaration -> named_context_val -> named_context_val
+ Context.Named.Declaration.t -> named_context_val -> named_context_val
(** Looks up in the context of local vars referred by names ([named_context])
raises [Not_found] if the Id.t is not found *)
-val lookup_named : variable -> env -> named_declaration
-val lookup_named_val : variable -> named_context_val -> named_declaration
+val lookup_named : variable -> env -> Context.Named.Declaration.t
+val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t
val evaluable_named : variable -> env -> bool
val named_type : variable -> env -> types
val named_body : variable -> env -> constr option
@@ -107,11 +106,11 @@ val named_body : variable -> env -> constr option
(** {6 Recurrence on [named_context]: older declarations processed first } *)
val fold_named_context :
- (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+ (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
(** Recurrence on [named_context] starting from younger decl *)
val fold_named_context_reverse :
- ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a
+ ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a
(** This forgets named and rel contexts *)
val reset_context : env -> env
@@ -228,7 +227,7 @@ val vars_of_global : env -> constr -> Id.Set.t
val really_needed : env -> Id.Set.t -> Id.Set.t
(** like [really_needed] but computes a well ordered named context *)
-val keep_hyps : env -> Id.Set.t -> section_context
+val keep_hyps : env -> Id.Set.t -> Context.section_context
(** {5 Unsafe judgments. }
We introduce here the pre-type of judgments, which is
@@ -258,22 +257,22 @@ exception Hyp_not_found
return [tail::(f head (id,_,_) (rev tail))::head].
the value associated to id should not change *)
val apply_to_hyp : named_context_val -> variable ->
- (named_context -> named_declaration -> named_context -> named_declaration) ->
+ (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) ->
named_context_val
(** [apply_to_hyp_and_dependent_on sign id f g] split [sign] into
[tail::(id,_,_)::head] and
return [(g tail)::(f (id,_,_))::head]. *)
val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
- (named_declaration -> named_context_val -> named_declaration) ->
- (named_declaration -> named_context_val -> named_declaration) ->
+ (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) ->
+ (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) ->
named_context_val
val insert_after_hyp : named_context_val -> variable ->
- named_declaration ->
- (named_context -> unit) -> named_context_val
+ Context.Named.Declaration.t ->
+ (Context.Named.t -> unit) -> named_context_val
-val remove_hyps : Id.Set.t -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
+val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index b625478f2..85c74534e 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -90,7 +90,7 @@ let judge_of_variable env id =
variables of the current env *)
(* TODO: check order? *)
let check_hyps_inclusion env f c sign =
- Context.fold_named_context
+ Context.Named.fold_outside
(fun (id,_,ty1) () ->
try
let ty2 = named_type id env in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 11df40caf..da2d213ff 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -12,7 +12,6 @@ open Names
open Univ
open Term
open Vars
-open Context
open Declarations
open Declareops
open Inductive
@@ -341,7 +340,7 @@ let typecheck_inductive env mie =
type ill_formed_ind =
| LocalNonPos of int
| LocalNotEnoughArgs of int
- | LocalNotConstructor of rel_context * constr list
+ | LocalNotConstructor of Context.Rel.t * constr list
| LocalNonPar of int * int * int
exception IllFormedInd of ill_formed_ind
@@ -361,7 +360,7 @@ let explain_ind_err id ntyp env nbpar c err =
raise (InductiveError
(NotEnoughArgs (env,c',mkRel (kt+nbpar))))
| LocalNotConstructor (paramsctxt,args)->
- let nparams = rel_context_nhyps paramsctxt in
+ let nparams = Context.Rel.nhyps paramsctxt in
raise (InductiveError
(NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,
List.length args - nparams)))
@@ -384,7 +383,7 @@ let failwith_non_pos_list n ntypes l =
(* Check the inductive type is called with the expected parameters *)
let check_correct_par (env,n,ntypes,_) hyps l largs =
- let nparams = rel_context_nhyps hyps in
+ let nparams = Context.Rel.nhyps hyps in
let largs = Array.of_list largs in
if Array.length largs < nparams then
raise (IllFormedInd (LocalNotEnoughArgs l));
@@ -465,8 +464,8 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
arguments (used to generate induction schemes, so a priori less
relevant to the kernel). *)
let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
- let lparams = rel_context_length hyps in
- let nmr = rel_context_nhyps hyps in
+ let lparams = Context.Rel.length hyps in
+ let nmr = Context.Rel.nhyps hyps in
(** Positivity of one argument [c] of a constructor (i.e. the
constructor [cn] has a type of the shape [… -> c … -> P], where,
more generally, the arrows may be dependent). *)
@@ -617,13 +616,13 @@ let check_positivity kn env_ar params inds =
let ntypes = Array.length inds in
let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
let lra_ind = Array.rev_to_list rc in
- let lparams = rel_context_length params in
- let nmr = rel_context_nhyps params in
+ let lparams = Context.Rel.length params in
+ let nmr = Context.Rel.nhyps params in
let check_one i (_,lcnames,lc,(sign,_)) =
let ra_env =
List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
- let nargs = rel_context_nhyps sign - nmr in
+ let nargs = Context.Rel.nhyps sign - nmr in
check_positivity_one ienv params (kn,i) nargs lcnames lc
in
let irecargs_nmr = Array.mapi check_one inds in
@@ -697,7 +696,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
matching with a parameter context. *)
let indty, paramsletsubst =
(* [ty] = [Ind inst] is typed in context [params] *)
- let inst = extended_rel_vect 0 paramslet in
+ let inst = Context.Rel.to_extended_vect 0 paramslet in
let ty = mkApp (mkIndU indu, inst) in
(* [Ind inst] is typed in context [params-wo-let] *)
let inst' = rel_list 0 nparamargs in
@@ -710,7 +709,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
in
let ci =
let print_info =
- { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
+ { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
{ ci_ind = ind;
ci_npar = nparamargs;
ci_cstr_ndecls = mind_consnrealdecls;
@@ -783,8 +782,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
let hyps = used_section_variables env inds in
- let nparamargs = rel_context_nhyps params in
- let nparamdecls = rel_context_length params in
+ let nparamargs = Context.Rel.nhyps params in
+ let nparamdecls = Context.Rel.length params in
let subst, ctx = Univ.abstract_universes p ctx in
let params = Vars.subst_univs_level_context subst params in
let env_ar =
@@ -799,10 +798,10 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
let consnrealdecls =
- Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
+ Array.map (fun (d,_) -> Context.Rel.length d - Context.Rel.length params)
splayed_lc in
let consnrealargs =
- Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params)
+ Array.map (fun (d,_) -> Context.Rel.nhyps d - Context.Rel.nhyps params)
splayed_lc in
(* Elimination sorts *)
let arkind,kelim =
@@ -835,8 +834,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
{ mind_typename = id;
mind_arity = arkind;
mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign;
- mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
- mind_nrealdecls = rel_context_length ar_sign - nparamdecls;
+ mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs;
+ mind_nrealdecls = Context.Rel.length ar_sign - nparamdecls;
mind_kelim = kelim;
mind_consnames = Array.of_list cnames;
mind_consnrealdecls = consnrealdecls;
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 01acdce5c..1fe47b1a5 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -42,6 +42,6 @@ val enforce_indices_matter : unit -> unit
val is_indices_matter : unit -> bool
val compute_projections : pinductive -> Id.t -> Id.t ->
- int -> Context.rel_context -> int array -> int array ->
- Context.rel_context -> Context.rel_context ->
+ int -> Context.Rel.t -> int array -> int array ->
+ Context.Rel.t -> Context.Rel.t ->
(constant array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d0df5c7b3..7bf1bfeb2 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -12,7 +12,6 @@ open Names
open Univ
open Term
open Vars
-open Context
open Declarations
open Declareops
open Environ
@@ -77,7 +76,7 @@ let instantiate_params full t u args sign =
let fail () =
anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
let (rem_args, subs, ty) =
- Context.fold_rel_context
+ Context.Rel.fold_outside
(fun (_,copt,_) (largs,subs,ty) ->
match (copt, largs, kind_of_term ty) with
| (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
@@ -297,7 +296,7 @@ let build_dependent_inductive ind (_,mip) params =
applist
(mkIndU ind,
List.map (lift mip.mind_nrealdecls) params
- @ extended_rel_list 0 realargs)
+ @ Context.Rel.to_extended_list 0 realargs)
(* This exception is local *)
exception LocalArity of (sorts_family * sorts_family * arity_error) option
@@ -350,12 +349,12 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
let build_one_branch i cty =
let typi = full_constructor_instantiate (ind,u,specif,params) cty in
let (cstrsign,ccl) = decompose_prod_assum typi in
- let nargs = rel_context_length cstrsign in
+ let nargs = Context.Rel.length cstrsign in
let (_,allargs) = decompose_app ccl in
let (lparams,vargs) = List.chop (inductive_params specif) allargs in
let cargs =
let cstr = ith_constructor_of_inductive ind (i+1) in
- let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in
+ let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in
vargs @ [dep_cstr] in
let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
it_mkProd_or_LetIn base cstrsign in
@@ -499,7 +498,7 @@ let subterm_var p renv =
with Failure _ | Invalid_argument _ -> Not_subterm
let push_ctxt_renv renv ctxt =
- let n = rel_context_length ctxt in
+ let n = Context.Rel.length ctxt in
{ env = push_rel_context ctxt renv.env;
rel_min = renv.rel_min+n;
genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv }
@@ -701,7 +700,7 @@ let restrict_spec env spec p =
else let absctx, ar = dest_lam_assum env p in
(* Optimization: if the predicate is not dependent, no restriction is needed
and we avoid building the recargs tree. *)
- if noccur_with_meta 1 (rel_context_length absctx) ar then spec
+ if noccur_with_meta 1 (Context.Rel.length absctx) ar then spec
else
let env = push_rel_context absctx env in
let arctx, s = dest_prod_assum env ar in
@@ -843,7 +842,7 @@ let filter_stack_domain env ci p stack =
let absctx, ar = dest_lam_assum env p in
(* Optimization: if the predicate is not dependent, no restriction is needed
and we avoid building the recargs tree. *)
- if noccur_with_meta 1 (rel_context_length absctx) ar then stack
+ if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack
else let env = push_rel_context absctx env in
let rec filter_stack env ar stack =
let t = whd_betadeltaiota env ar in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 5847d25f6..541fb8282 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Univ
open Declarations
open Environ
@@ -35,7 +34,7 @@ val lookup_mind_specif : env -> inductive -> mind_specif
(** {6 Functions to build standard types related to inductive } *)
val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
-val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context
+val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t
val instantiate_inductive_constraints :
mutual_inductive_body -> universe_instance -> constraints
@@ -86,7 +85,7 @@ val build_branches_type :
constr list -> constr -> types array
(** Return the arity of an inductive type *)
-val mind_arity : one_inductive_body -> rel_context * sorts_family
+val mind_arity : one_inductive_body -> Context.Rel.t * sorts_family
val inductive_sort_family : one_inductive_body -> sorts_family
@@ -111,8 +110,8 @@ exception SingletonInductiveBecomesProp of Id.t
val max_inductive_sort : sorts array -> universe
-val instantiate_universes : env -> rel_context ->
- template_arity -> constr Lazy.t array -> rel_context * sorts
+val instantiate_universes : env -> Context.Rel.t ->
+ template_arity -> constr Lazy.t array -> Context.Rel.t * sorts
(** {6 Debug} *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 98b2d6d2e..dd6ef1c66 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -8,7 +8,6 @@
open Errors
open Names
open Term
-open Context
open Declarations
open Util
open Nativevalues
@@ -1826,15 +1825,15 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
in
let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
let auxdefs = List.fold_right get_named_val fv_named auxdefs in
- let lvl = rel_context_length env.env_rel_context in
+ let lvl = Context.Rel.length env.env_rel_context in
let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in
let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in
let aux_name = fresh_lname Anonymous in
auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))
and compile_rel env sigma univ auxdefs n =
- let (_,body,_) = lookup_rel n env.env_rel_context in
- let n = rel_context_length env.env_rel_context - n in
+ let (_,body,_) = Context.Rel.lookup n env.env_rel_context in
+ let n = Context.Rel.length env.env_rel_context - n in
match body with
| Some t ->
let code = lambda_of_constr env sigma t in
@@ -1844,7 +1843,7 @@ and compile_rel env sigma univ auxdefs n =
Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs
and compile_named env sigma univ auxdefs id =
- let (_,body,_) = lookup_named id env.env_named_context in
+ let (_,body,_) = Context.Named.lookup id env.env_named_context in
match body with
| Some t ->
let code = lambda_of_constr env sigma t in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index badb15b56..bfddf8286 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t }
+ abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t }
type proofterm = (constr * Univ.universe_context_set) Future.computation
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 009ff82ff..5b743a4c7 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -48,7 +48,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t }
+ abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t }
(* The type has two caveats:
1) cook_constr is defined after
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 615b9d49b..9fcec1114 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -15,7 +15,6 @@
open Util
open Names
-open Context
open Univ
open Term
open Declarations
@@ -66,9 +65,9 @@ type named_vals = (Id.t * lazy_val) list
type env = {
env_globals : globals;
- env_named_context : named_context;
+ env_named_context : Context.Named.t;
env_named_vals : named_vals;
- env_rel_context : rel_context;
+ env_rel_context : Context.Rel.t;
env_rel_val : lazy_val list;
env_nb_rel : int;
env_stratification : stratification;
@@ -77,7 +76,7 @@ type env = {
indirect_pterms : Opaqueproof.opaquetab;
}
-type named_context_val = named_context * named_vals
+type named_context_val = Context.Named.t * named_vals
let empty_named_context_val = [],[]
@@ -87,9 +86,9 @@ let empty_env = {
env_inductives = Mindmap_env.empty;
env_modules = MPmap.empty;
env_modtypes = MPmap.empty};
- env_named_context = empty_named_context;
+ env_named_context = Context.Named.empty;
env_named_vals = [];
- env_rel_context = empty_rel_context;
+ env_rel_context = Context.Rel.empty;
env_rel_val = [];
env_nb_rel = 0;
env_stratification = {
@@ -107,7 +106,7 @@ let nb_rel env = env.env_nb_rel
let push_rel d env =
let rval = ref VKnone in
{ env with
- env_rel_context = add_rel_decl d env.env_rel_context;
+ env_rel_context = Context.Rel.add d env.env_rel_context;
env_rel_val = rval :: env.env_rel_val;
env_nb_rel = env.env_nb_rel + 1 }
@@ -127,7 +126,7 @@ let env_of_rel n env =
let push_named_context_val d (ctxt,vals) =
let id,_,_ = d in
let rval = ref VKnone in
- add_named_decl d ctxt, (id,rval)::vals
+ Context.Named.add d ctxt, (id,rval)::vals
let push_named d env =
(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
@@ -135,7 +134,7 @@ let push_named d env =
let id,body,_ = d in
let rval = ref VKnone in
{ env_globals = env.env_globals;
- env_named_context = Context.add_named_decl d env.env_named_context;
+ env_named_context = Context.Named.add d env.env_named_context;
env_named_vals = (id, rval) :: env.env_named_vals;
env_rel_context = env.env_rel_context;
env_rel_val = env.env_rel_val;
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index f40311661..1e95a3564 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Declarations
(** The type of environments. *)
@@ -45,9 +44,9 @@ type named_vals = (Id.t * lazy_val) list
type env = {
env_globals : globals;
- env_named_context : named_context;
+ env_named_context : Context.Named.t;
env_named_vals : named_vals;
- env_rel_context : rel_context;
+ env_rel_context : Context.Rel.t;
env_rel_val : lazy_val list;
env_nb_rel : int;
env_stratification : stratification;
@@ -56,7 +55,7 @@ type env = {
indirect_pterms : Opaqueproof.opaquetab;
}
-type named_context_val = named_context * named_vals
+type named_context_val = Context.Named.t * named_vals
val empty_named_context_val : named_context_val
@@ -65,15 +64,15 @@ val empty_env : env
(** Rel context *)
val nb_rel : env -> int
-val push_rel : rel_declaration -> env -> env
+val push_rel : Context.Rel.Declaration.t -> env -> env
val lookup_rel_val : int -> env -> lazy_val
val env_of_rel : int -> env -> env
(** Named context *)
val push_named_context_val :
- named_declaration -> named_context_val -> named_context_val
-val push_named : named_declaration -> env -> env
+ Context.Named.Declaration.t -> named_context_val -> named_context_val
+val push_named : Context.Named.Declaration.t -> env -> env
val lookup_named_val : Id.t -> env -> lazy_val
val env_of_named : Id.t -> env -> env
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index bf2ee2707..78222c6b6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -20,7 +20,6 @@ open Util
open Names
open Term
open Vars
-open Context
open Univ
open Environ
open Closure
@@ -741,10 +740,10 @@ let dest_prod env =
match kind_of_term t with
| Prod (n,a,c0) ->
let d = (n,None,a) in
- decrec (push_rel d env) (add_rel_decl d m) c0
+ decrec (push_rel d env) (Context.Rel.add d m) c0
| _ -> m,t
in
- decrec env empty_rel_context
+ decrec env Context.Rel.empty
(* The same but preserving lets in the context, not internal ones. *)
let dest_prod_assum env =
@@ -753,17 +752,17 @@ let dest_prod_assum env =
match kind_of_term rty with
| Prod (x,t,c) ->
let d = (x,None,t) in
- prodec_rec (push_rel d env) (add_rel_decl d l) c
+ prodec_rec (push_rel d env) (Context.Rel.add d l) c
| LetIn (x,b,t,c) ->
let d = (x,Some b,t) in
- prodec_rec (push_rel d env) (add_rel_decl d l) c
+ prodec_rec (push_rel d env) (Context.Rel.add d l) c
| Cast (c,_,_) -> prodec_rec env l c
| _ ->
let rty' = whd_betadeltaiota env rty in
if Term.eq_constr rty' rty then l, rty
else prodec_rec env l rty'
in
- prodec_rec env empty_rel_context
+ prodec_rec env Context.Rel.empty
let dest_lam_assum env =
let rec lamec_rec env l ty =
@@ -771,14 +770,14 @@ let dest_lam_assum env =
match kind_of_term rty with
| Lambda (x,t,c) ->
let d = (x,None,t) in
- lamec_rec (push_rel d env) (add_rel_decl d l) c
+ lamec_rec (push_rel d env) (Context.Rel.add d l) c
| LetIn (x,b,t,c) ->
let d = (x,Some b,t) in
- lamec_rec (push_rel d env) (add_rel_decl d l) c
+ lamec_rec (push_rel d env) (Context.Rel.add d l) c
| Cast (c,_,_) -> lamec_rec env l c
| _ -> l,rty
in
- lamec_rec env empty_rel_context
+ lamec_rec env Context.Rel.empty
exception NotArity
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index f7a8d88c2..35daff7b5 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Term
-open Context
open Environ
(***********************************************************************
@@ -99,9 +98,9 @@ val betazeta_appvect : int -> constr -> constr array -> constr
(***********************************************************************
s Recognizing products and arities modulo reduction *)
-val dest_prod : env -> types -> rel_context * types
-val dest_prod_assum : env -> types -> rel_context * types
-val dest_lam_assum : env -> types -> rel_context * types
+val dest_prod : env -> types -> Context.Rel.t * types
+val dest_prod_assum : env -> types -> Context.Rel.t * types
+val dest_lam_assum : env -> types -> Context.Rel.t * types
exception NotArity
diff --git a/kernel/term.ml b/kernel/term.ml
index 2060c7b6e..24f82a9ec 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -10,7 +10,6 @@ open Util
open Pp
open Errors
open Names
-open Context
open Vars
(**********************************************************************)
@@ -579,24 +578,24 @@ let decompose_lam_n n =
let decompose_prod_assum =
let rec prodec_rec l c =
match kind_of_term c with
- | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) c
- | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c
+ | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) c
+ | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) c
| Cast (c,_,_) -> prodec_rec l c
| _ -> l,c
in
- prodec_rec empty_rel_context
+ prodec_rec Context.Rel.empty
(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
let decompose_lam_assum =
let rec lamdec_rec l c =
match kind_of_term c with
- | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) c
- | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) c
| Cast (c,_,_) -> lamdec_rec l c
| _ -> l,c
in
- lamdec_rec empty_rel_context
+ lamdec_rec Context.Rel.empty
(* Given a positive integer n, decompose a product or let-in term
of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair
@@ -608,12 +607,12 @@ let decompose_prod_n_assum n =
let rec prodec_rec l n c =
if Int.equal n 0 then l,c
else match kind_of_term c with
- | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c
- | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+ | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) (n-1) c
+ | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c
| Cast (c,_,_) -> prodec_rec l n c
| c -> error "decompose_prod_n_assum: not enough assumptions"
in
- prodec_rec empty_rel_context n
+ prodec_rec Context.Rel.empty n
(* Given a positive integer n, decompose a lambda or let-in term [fun
(x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted
@@ -627,12 +626,12 @@ let decompose_lam_n_assum n =
let rec lamdec_rec l n c =
if Int.equal n 0 then l,c
else match kind_of_term c with
- | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
- | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) n c
| Cast (c,_,_) -> lamdec_rec l n c
| c -> error "decompose_lam_n_assum: not enough abstractions"
in
- lamdec_rec empty_rel_context n
+ lamdec_rec Context.Rel.empty n
(* Same, counting let-in *)
let decompose_lam_n_decls n =
@@ -641,12 +640,12 @@ let decompose_lam_n_decls n =
let rec lamdec_rec l n c =
if Int.equal n 0 then l,c
else match kind_of_term c with
- | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
- | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c
| Cast (c,_,_) -> lamdec_rec l n c
| c -> error "decompose_lam_n_decls: not enough abstractions"
in
- lamdec_rec empty_rel_context n
+ lamdec_rec Context.Rel.empty n
let prod_assum t = fst (decompose_prod_assum t)
let prod_n_assum n t = fst (decompose_prod_n_assum n t)
@@ -667,7 +666,7 @@ let strip_lam_n n t = snd (decompose_lam_n n t)
Such a term can canonically be seen as the pair of a context of types
and of a sort *)
-type arity = rel_context * sorts
+type arity = Context.Rel.t * sorts
let destArity =
let rec prodec_rec l c =
diff --git a/kernel/term.mli b/kernel/term.mli
index 972a67ebe..c45e04338 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Context
(** {5 Redeclaration of types from module Constr and Sorts}
@@ -213,14 +212,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
val mkNamedProd : Id.t -> types -> types -> types
(** Constructs either [(x:t)c] or [[x=b:t]c] *)
-val mkProd_or_LetIn : rel_declaration -> types -> types
-val mkProd_wo_LetIn : rel_declaration -> types -> types
-val mkNamedProd_or_LetIn : named_declaration -> types -> types
-val mkNamedProd_wo_LetIn : named_declaration -> types -> types
+val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types
+val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types
(** Constructs either [[x:t]c] or [[x=b:t]c] *)
-val mkLambda_or_LetIn : rel_declaration -> constr -> constr
-val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
+val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr
+val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr
(** {5 Other term constructors. } *)
@@ -262,8 +261,8 @@ val to_lambda : int -> constr -> constr
where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *)
val to_prod : int -> constr -> constr
-val it_mkLambda_or_LetIn : constr -> rel_context -> constr
-val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
+val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
(** In [lambda_applist c args], [c] is supposed to have the form
[λΓ.c] with [Γ] without let-in; it returns [c] with the variables
@@ -314,29 +313,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
(** Extract the premisses and the conclusion of a term of the form
"(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
-val decompose_prod_assum : types -> rel_context * types
+val decompose_prod_assum : types -> Context.Rel.t * types
(** Idem with lambda's *)
-val decompose_lam_assum : constr -> rel_context * constr
+val decompose_lam_assum : constr -> Context.Rel.t * constr
(** Idem but extract the first [n] premisses, counting let-ins. *)
-val decompose_prod_n_assum : int -> types -> rel_context * types
+val decompose_prod_n_assum : int -> types -> Context.Rel.t * types
(** Idem for lambdas, _not_ counting let-ins *)
-val decompose_lam_n_assum : int -> constr -> rel_context * constr
+val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr
(** Idem, counting let-ins *)
-val decompose_lam_n_decls : int -> constr -> rel_context * constr
+val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr
(** Return the premisses/parameters of a type/term (let-in included) *)
-val prod_assum : types -> rel_context
-val lam_assum : constr -> rel_context
+val prod_assum : types -> Context.Rel.t
+val lam_assum : constr -> Context.Rel.t
(** Return the first n-th premisses/parameters of a type (let included and counted) *)
-val prod_n_assum : int -> types -> rel_context
+val prod_n_assum : int -> types -> Context.Rel.t
(** Return the first n-th premisses/parameters of a term (let included but not counted) *)
-val lam_n_assum : int -> constr -> rel_context
+val lam_n_assum : int -> constr -> Context.Rel.t
(** Remove the premisses/parameters of a type/term *)
val strip_prod : types -> types
@@ -369,7 +368,7 @@ val under_outer_cast : (constr -> constr) -> constr -> constr
Such a term can canonically be seen as the pair of a context of types
and of a sort *)
-type arity = rel_context * sorts
+type arity = Context.Rel.t * sorts
(** Build an "arity" from its canonical form *)
val mkArity : arity -> types
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index aa60432a7..a4e119f0b 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -16,7 +16,6 @@ open Errors
open Util
open Names
open Term
-open Context
open Declarations
open Environ
open Entries
@@ -246,8 +245,8 @@ let infer_declaration ~trust env kn dcl =
let global_vars_set_constant_type env = function
| RegularArity t -> global_vars_set env t
| TemplateArity (ctx,_) ->
- Context.fold_rel_context
- (fold_rel_declaration
+ Context.Rel.fold_outside
+ (Context.Rel.Declaration.fold
(fun t c -> Id.Set.union (global_vars_set env t) c))
ctx ~init:Id.Set.empty
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4f32fdce8..35f53b7e7 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -12,7 +12,6 @@ open Names
open Univ
open Term
open Vars
-open Context
open Declarations
open Environ
open Entries
@@ -99,7 +98,7 @@ let judge_of_variable env id =
variables of the current env.
Order does not have to be checked assuming that all names are distinct *)
let check_hyps_inclusion env c sign =
- Context.fold_named_context
+ Context.Named.fold_outside
(fun (id,b1,ty1) () ->
try
let (_,b2,ty2) = lookup_named id env in
@@ -561,6 +560,6 @@ let infer_local_decls env decls =
| (id, d) :: l ->
let (env, l) = inferec env l in
let d = infer_local_decl env id d in
- (push_rel d env, add_rel_decl d l)
- | [] -> (env, empty_rel_context) in
+ (push_rel d env, Context.Rel.add d l)
+ | [] -> (env, Context.Rel.empty) in
inferec env decls
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 010b2b6f0..bcaa6b63e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -9,7 +9,6 @@
open Names
open Univ
open Term
-open Context
open Environ
open Entries
open Declarations
@@ -28,7 +27,7 @@ val infer_v : env -> constr array -> unsafe_judgment array
val infer_type : env -> types -> unsafe_type_judgment
val infer_local_decls :
- env -> (Id.t * local_entry) list -> (env * rel_context)
+ env -> (Id.t * local_entry) list -> (env * Context.Rel.t)
(** {6 Basic operations of the typing machine. } *)
@@ -128,4 +127,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
constant_type
(** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> constr -> section_context -> unit
+val check_hyps_inclusion : env -> constr -> Context.section_context -> unit
diff --git a/kernel/vars.ml b/kernel/vars.ml
index a00c7036f..53543e043 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -8,7 +8,6 @@
open Names
open Esubst
-open Context
(*********************)
(* Occurring *)
@@ -160,9 +159,9 @@ let substnl laml n c = substn_many (make_subst laml) n c
let substl laml c = substn_many (make_subst laml) 0 c
let subst1 lam c = substn_many [|make_substituend lam|] 0 c
-let substnl_decl laml k r = map_rel_declaration (fun c -> substnl laml k c) r
-let substl_decl laml r = map_rel_declaration (fun c -> substnl laml 0 c) r
-let subst1_decl lam r = map_rel_declaration (fun c -> subst1 lam c) r
+let substnl_decl laml k r = Context.Rel.Declaration.map (fun c -> substnl laml k c) r
+let substl_decl laml r = Context.Rel.Declaration.map (fun c -> substnl laml 0 c) r
+let subst1_decl lam r = Context.Rel.Declaration.map (fun c -> subst1 lam c) r
(* Build a substitution from an instance, inserting missing let-ins *)
@@ -302,7 +301,7 @@ let subst_univs_level_constr subst c =
if !changed then c' else c
let subst_univs_level_context s =
- map_rel_context (subst_univs_level_constr s)
+ Context.Rel.map (subst_univs_level_constr s)
let subst_instance_constr subst c =
if Univ.Instance.is_empty subst then c
@@ -343,7 +342,7 @@ let subst_instance_constr subst c =
let subst_instance_context s ctx =
if Univ.Instance.is_empty s then ctx
- else map_rel_context (fun x -> subst_instance_constr s x) ctx
+ else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
type id_key = constant tableKey
let eq_id_key x y = Names.eq_table_key Constant.equal x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index a84cf0114..659990806 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -8,7 +8,6 @@
open Names
open Constr
-open Context
(** {6 Occur checks } *)
@@ -69,10 +68,10 @@ type substl = constr list
as if usable in [applist] while the substitution is
represented the other way round, i.e. ending with either [u₁] or
[c₁], as if usable for [substl]. *)
-val subst_of_rel_context_instance : rel_context -> constr list -> substl
+val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl
(** For compatibility: returns the substitution reversed *)
-val adjust_subst_to_rel_context : rel_context -> constr list -> constr list
+val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list
(** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an]
for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
@@ -92,13 +91,13 @@ val subst1 : constr -> constr -> constr
accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if
Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then
Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *)
-val substnl_decl : substl -> int -> rel_declaration -> rel_declaration
+val substnl_decl : substl -> int -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
(** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *)
-val substl_decl : substl -> rel_declaration -> rel_declaration
+val substl_decl : substl -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
(** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *)
-val subst1_decl : constr -> rel_declaration -> rel_declaration
+val subst1_decl : constr -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
(** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by
[cj] in [t]. *)
@@ -136,11 +135,11 @@ val subst_univs_constr : universe_subst -> constr -> constr
(** Level substitutions for polymorphism. *)
val subst_univs_level_constr : universe_level_subst -> constr -> constr
-val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context
+val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t
(** Instance substitution for polymorphism. *)
val subst_instance_constr : universe_instance -> constr -> constr
-val subst_instance_context : universe_instance -> rel_context -> rel_context
+val subst_instance_context : universe_instance -> Context.Rel.t -> Context.Rel.t
type id_key = constant tableKey
val eq_id_key : id_key -> id_key -> bool
diff --git a/library/decls.ml b/library/decls.ml
index 8d5085f70..b5f9143b8 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -11,7 +11,6 @@
open Util
open Names
-open Context
open Decl_kinds
open Libnames
@@ -55,7 +54,7 @@ let initialize_named_context_for_proof () =
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
let last_section_hyps dir =
- fold_named_context
+ Context.Named.fold_outside
(fun (id,_,_) sec_ids ->
try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
with Not_found -> sec_ids)
diff --git a/library/global.mli b/library/global.mli
index 09ed4eb0a..d6547105d 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -21,7 +21,7 @@ val env_is_initial : unit -> bool
val universes : unit -> UGraph.t
val named_context_val : unit -> Environ.named_context_val
-val named_context : unit -> Context.named_context
+val named_context : unit -> Context.Named.t
(** {6 Enriching the global environment } *)
@@ -73,7 +73,7 @@ val add_module_parameter :
(** {6 Queries in the global environment } *)
-val lookup_named : variable -> Context.named_declaration
+val lookup_named : variable -> Context.Named.Declaration.t
val lookup_constant : constant -> Declarations.constant_body
val lookup_inductive : inductive ->
Declarations.mutual_inductive_body * Declarations.one_inductive_body
diff --git a/library/lib.mli b/library/lib.mli
index bb8831759..874fc89fb 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -164,7 +164,7 @@ type variable_context = variable_info list
type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
val instance_from_variable_context : variable_context -> Names.Id.t array
-val named_of_variable_context : variable_context -> Context.named_context
+val named_of_variable_context : variable_context -> Context.Named.t
val section_segment_of_constant : Names.constant -> abstr_info
val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info
@@ -175,8 +175,8 @@ val is_in_section : Globnames.global_reference -> bool
val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
val add_section_context : Univ.universe_context_set -> unit
val add_section_constant : bool (* is_projection *) ->
- Names.constant -> Context.named_context -> unit
-val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit
+ Names.constant -> Context.Named.t -> unit
+val add_section_kn : Names.mutual_inductive -> Context.Named.t -> unit
val replacement_context : unit -> Opaqueproof.work_list
(** {6 Discharge: decrease the section level if in the current section } *)
@@ -189,6 +189,6 @@ val discharge_inductive : Names.inductive -> Names.inductive
(* discharging a constant in one go *)
val full_replacement_context : unit -> Opaqueproof.work_list list
val full_section_segment_of_constant :
- Names.constant -> (Context.named_context -> Context.named_context) list
+ Names.constant -> (Context.Named.t -> Context.Named.t) list
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 2dc2420c4..923743ece 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -11,7 +11,6 @@ open Util
open Names
open Term
open Vars
-open Context
open Declarations
open Declareops
open Environ
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 6c7b09383..d306112ce 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Term
-open Context
open Globnames
val qflag : bool ref
@@ -27,7 +26,7 @@ type counter = bool -> metavariable
val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
val ind_hyps : int -> pinductive -> constr list ->
- Proof_type.goal Tacmach.sigma -> rel_context array
+ Proof_type.goal Tacmach.sigma -> Context.Rel.t array
type atoms = {positive:constr list;negative:constr list}
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 1474f1e93..4eab5f912 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -3,7 +3,6 @@ open Errors
open Util
open Term
open Vars
-open Context
open Namegen
open Names
open Declarations
@@ -230,7 +229,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
-let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
+let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
let nochange ?t' msg =
begin
observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index bbe2f1a3a..e2c3bbb97 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -3,7 +3,6 @@ open Errors
open Util
open Term
open Vars
-open Context
open Namegen
open Names
open Pp
@@ -30,7 +29,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let env = Global.env () in
let env_with_params = Environ.push_rel_context princ_type_info.params env in
let tbl = Hashtbl.create 792 in
- let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context) : rel_context =
+ let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t =
match predicates with
| [] -> []
|(Name x,v,t)::predicates ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5d92fca5e..80de8e764 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env =
let new_env = add_pat_variables env pat typ in
let res =
fst (
- Context.fold_rel_context
+ Context.Rel.fold_outside
(fun (na,v,t) (env,ctxt) ->
match na with
| Anonymous -> assert false
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index e3455e770..be04728e0 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -19,7 +19,6 @@ open Pp
open Names
open Term
open Vars
-open Context
open Termops
open Declarations
open Glob_term
@@ -258,27 +257,27 @@ type merge_infos =
lnk2: int merged_arg array;
(** rec params which remain rec param (ie not linked) *)
- recprms1: rel_declaration list;
- recprms2: rel_declaration list;
+ recprms1: Context.Rel.Declaration.t list;
+ recprms2: Context.Rel.Declaration.t list;
nrecprms1: int;
nrecprms2: int;
(** rec parms which became non parm (either linked to something
or because after a rec parm that became non parm) *)
- otherprms1: rel_declaration list;
- otherprms2: rel_declaration list;
+ otherprms1: Context.Rel.Declaration.t list;
+ otherprms2: Context.Rel.Declaration.t list;
notherprms1:int;
notherprms2:int;
(** args which remain args in merge *)
- args1:rel_declaration list;
- args2:rel_declaration list;
+ args1:Context.Rel.Declaration.t list;
+ args2:Context.Rel.Declaration.t list;
nargs1:int;
nargs2:int;
(** functional result args *)
- funresprms1: rel_declaration list;
- funresprms2: rel_declaration list;
+ funresprms1: Context.Rel.Declaration.t list;
+ funresprms2: Context.Rel.Declaration.t list;
nfunresprms1:int;
nfunresprms2:int;
}
@@ -851,7 +850,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
lident , bindlist , Some cstr_expr , lcstor_expr
-let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
+let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
match rdecl with
| (nme,None,t) ->
let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b894cb8ea..adcaa6441 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -13,7 +13,6 @@ open Names
open Nameops
open Term
open Vars
-open Context
open Termops
open Namegen
open Declarations
@@ -131,7 +130,7 @@ type tomatch_status =
| Pushed of (bool*((constr * tomatch_type) * int list * Name.t))
| Alias of (bool*(Name.t * constr * (constr * types)))
| NonDepAlias
- | Abstract of int * rel_declaration
+ | Abstract of int * Context.Rel.Declaration.t
type tomatch_stack = tomatch_status list
@@ -602,7 +601,7 @@ let relocate_index_tomatch n1 n2 =
NonDepAlias :: genrec depth rest
| Abstract (i,d) :: rest ->
let i = relocate_rel n1 n2 depth i in
- Abstract (i,map_rel_declaration (relocate_index n1 n2 depth) d)
+ Abstract (i, Context.Rel.Declaration.map (relocate_index n1 n2 depth) d)
:: genrec (depth+1) rest in
genrec 0
@@ -635,7 +634,7 @@ let replace_tomatch n c =
| NonDepAlias :: rest ->
NonDepAlias :: replrec depth rest
| Abstract (i,d) :: rest ->
- Abstract (i,map_rel_declaration (replace_term n c depth) d)
+ Abstract (i, Context.Rel.Declaration.map (replace_term n c depth) d)
:: replrec (depth+1) rest in
replrec 0
@@ -660,7 +659,7 @@ let rec liftn_tomatch_stack n depth = function
NonDepAlias :: liftn_tomatch_stack n depth rest
| Abstract (i,d)::rest ->
let i = if i<depth then i else i+n in
- Abstract (i,map_rel_declaration (liftn n depth) d)
+ Abstract (i, Context.Rel.Declaration.map (liftn n depth) d)
::(liftn_tomatch_stack n (depth+1) rest)
let lift_tomatch_stack n = liftn_tomatch_stack n 1
@@ -921,7 +920,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
let tms = List.fold_right2 (fun par arg tomatch ->
match kind_of_term par with
| Rel i -> relocate_index_tomatch (i+n) (destRel arg) tomatch
- | _ -> tomatch) (realargs@[cur]) (extended_rel_list 0 sign)
+ | _ -> tomatch) (realargs@[cur]) (Context.Rel.to_extended_list 0 sign)
(lift_tomatch_stack n tms) in
(* Pred is already dependent in the current term to match (if *)
(* (na<>Anonymous) and its realargs; we just need to adjust it to *)
@@ -1118,7 +1117,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with
| [], _ -> brs,tomatch,pred,[]
| n::deps, Abstract (i,d) :: tomatch ->
- let d = map_rel_declaration (nf_evar evd) d in
+ let d = Context.Rel.Declaration.map (nf_evar evd) d in
let is_d = match d with (_, None, _) -> false | _ -> true in
if is_d || List.exists (fun c -> dependent_decl (lift k c) d) tocheck
&& Array.exists (is_dependent_branch k) brs then
@@ -1187,7 +1186,7 @@ let group_equations pb ind current cstrs mat =
let rec generalize_problem names pb = function
| [] -> pb, []
| i::l ->
- let (na,b,t as d) = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
+ let (na,b,t as d) = Context.Rel.Declaration.map (lift i) (Environ.lookup_rel i pb.env) in
let pb',deps = generalize_problem names pb l in
begin match (na, b) with
| Anonymous, Some _ -> pb', deps
@@ -1230,7 +1229,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
(* We adjust the terms to match in the context they will be once the *)
(* context [x1:T1,..,xn:Tn] will have been pushed on the current env *)
let typs' =
- List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in
+ List.map_i (fun i d -> (mkRel i, Context.Rel.Declaration.map (lift i) d)) 1 typs in
let extenv = push_rel_context typs pb.env in
@@ -1560,8 +1559,8 @@ let matx_of_eqns env eqns =
*)
let adjust_to_extended_env_and_remove_deps env extenv subst t =
- let n = rel_context_length (rel_context env) in
- let n' = rel_context_length (rel_context extenv) in
+ let n = Context.Rel.length (rel_context env) in
+ let n' = Context.Rel.length (rel_context extenv) in
(* We first remove the bindings that are dependently typed (they are
difficult to manage and it is not sure these are so useful in practice);
Notes:
@@ -1673,8 +1672,8 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
| None ->
(* This is the situation we are building a return predicate and
we are in an impossible branch *)
- let n = rel_context_length (rel_context env) in
- let n' = rel_context_length (rel_context tycon_env) in
+ let n = Context.Rel.length (rel_context env) in
+ let n' = Context.Rel.length (rel_context tycon_env) in
let impossible_case_type, u =
e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in
(lift (n'-n) impossible_case_type, mkSort u)
@@ -1744,7 +1743,7 @@ let build_inversion_problem loc env sigma tms t =
let n = List.length sign in
let decls =
- List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in
+ List.map_i (fun i d -> (mkRel i, Context.Rel.Declaration.map (lift i) d)) 1 sign in
let pb_env = push_rel_context sign env in
let decls =
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index c599766ab..4ec71956b 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Evd
open Environ
open Inductiveops
@@ -45,11 +44,11 @@ val compile_cases :
val constr_of_pat :
Environ.env ->
Evd.evar_map ref ->
- rel_declaration list ->
+ Context.Rel.Declaration.t list ->
Glob_term.cases_pattern ->
Names.Id.t list ->
Glob_term.cases_pattern *
- (rel_declaration list * Term.constr *
+ (Context.Rel.Declaration.t list * Term.constr *
(Term.types * Term.constr list) * Glob_term.cases_pattern) *
Names.Id.t list
@@ -83,7 +82,7 @@ type tomatch_status =
| Pushed of (bool*((constr * tomatch_type) * int list * Name.t))
| Alias of (bool * (Name.t * constr * (constr * types)))
| NonDepAlias
- | Abstract of int * rel_declaration
+ | Abstract of int * Context.Rel.Declaration.t
type tomatch_stack = tomatch_status list
@@ -117,7 +116,7 @@ val prepare_predicate : Loc.t ->
Environ.env ->
Evd.evar_map ->
(Term.types * tomatch_type) list ->
- Context.rel_context list ->
+ Context.Rel.t list ->
Constr.constr option ->
'a option -> (Evd.evar_map * Names.name list * Term.constr) list
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5e99521a1..0b0bd8304 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -17,7 +17,6 @@ open Termops
open Reductionops
open Term
open Vars
-open Context
open Pattern
open Patternops
open Misctypes
@@ -269,8 +268,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in
let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in
- let n = rel_context_length ctx_b2 in
- let n' = rel_context_length ctx_b2' in
+ let n = Context.Rel.length ctx_b2 in
+ let n' = Context.Rel.length ctx_b2' in
if noccur_between 1 n b2 && noccur_between 1 n' b2' then
let f l (na,_,t) = (Anonymous,na,t)::l in
let ctx_br = List.fold_left f ctx ctx_b2 in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index dab82fa22..4ca066feb 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -12,7 +12,6 @@ open Util
open Names
open Term
open Vars
-open Context
open Inductiveops
open Environ
open Glob_term
@@ -199,7 +198,7 @@ let computable p k =
engendrera un prédicat non dépendant) *)
let sign,ccl = decompose_lam_assum p in
- Int.equal (rel_context_length sign) (k + 1)
+ Int.equal (Context.Rel.length sign) (k + 1)
&&
noccur_between 1 (k+1) ccl
@@ -315,7 +314,7 @@ let is_nondep_branch c l =
try
(* FIXME: do better using tags from l *)
let sign,ccl = decompose_lam_n_decls (List.length l) c in
- noccur_between 1 (rel_context_length sign) ccl
+ noccur_between 1 (Context.Rel.length sign) ccl
with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
false
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index eb158686a..f8f8093c0 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Environ
open Glob_term
open Termops
@@ -46,7 +45,7 @@ val detype_case :
val detype_sort : evar_map -> sorts -> glob_sort
val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) ->
- evar_map -> rel_context -> glob_decl list
+ evar_map -> Context.Rel.t -> glob_decl list
val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 69e8e9d98..af2877d34 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -11,7 +11,6 @@ open Errors
open Names
open Term
open Vars
-open Context
open Environ
open Termops
open Evd
@@ -501,7 +500,7 @@ let solve_pattern_eqn env l c =
match kind_of_term a with
(* Rem: if [a] links to a let-in, do as if it were an assumption *)
| Rel n ->
- let d = map_rel_declaration (lift n) (lookup_rel n env) in
+ let d = Context.Rel.Declaration.map (lift n) (lookup_rel n env) in
mkLambda_or_LetIn d c'
| Var id ->
let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 3c3afac54..f001d6e3e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -12,7 +12,6 @@ open Pp
open Names
open Term
open Vars
-open Context
open Termops
open Namegen
open Pre_env
@@ -78,12 +77,12 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
let env_nf_evar sigma env =
process_rel_context
- (fun d e -> push_rel (map_rel_declaration (nf_evar sigma) d) e) env
+ (fun d e -> push_rel (Context.Rel.Declaration.map (nf_evar sigma) d) e) env
let env_nf_betaiotaevar sigma env =
process_rel_context
(fun d e ->
- push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env
+ push_rel (Context.Rel.Declaration.map (Reductionops.nf_betaiota sigma) d) e) env
let nf_evars_universes evm =
Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm)
@@ -106,10 +105,10 @@ let nf_evar_map_universes evm =
Evd.raw_map (fun _ -> map_evar_info f) evm, f
let nf_named_context_evar sigma ctx =
- Context.map_named_context (nf_evar sigma) ctx
+ Context.Named.map (nf_evar sigma) ctx
let nf_rel_context_evar sigma ctx =
- Context.map_rel_context (nf_evar sigma) ctx
+ Context.Rel.map (nf_evar sigma) ctx
let nf_env_evar sigma env =
let nc' = nf_named_context_evar sigma (Environ.named_context env) in
@@ -303,7 +302,7 @@ let push_rel_context_to_named_context env typ =
(* with vars of the rel context *)
(* We do keep the instances corresponding to local definition (see above) *)
let (subst, vsubst, _, env) =
- Context.fold_rel_context
+ Context.Rel.fold_outside
(fun (na,c,t) (subst, vsubst, avoid, env) ->
let id =
(* ppedrot: we want to infer nicer names for the refine tactic, but
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 96648bb11..867917c9c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Evd
open Environ
@@ -129,7 +128,7 @@ val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.M
[nf_evar]. *)
val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
-val undefined_evars_of_named_context : evar_map -> named_context -> Evar.Set.t
+val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
(** [occur_evar_upto sigma k c] returns [true] if [k] appears in
@@ -170,8 +169,8 @@ val jv_nf_evar :
val tj_nf_evar :
evar_map -> unsafe_type_judgment -> unsafe_type_judgment
-val nf_named_context_evar : evar_map -> named_context -> named_context
-val nf_rel_context_evar : evar_map -> rel_context -> rel_context
+val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
+val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t
val nf_env_evar : evar_map -> env -> env
val nf_evar_info : evar_map -> evar_info -> evar_info
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 47d9654e5..1366c34ce 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Locus
-open Context
open Term
open Evd
open Pretype_errors
@@ -50,7 +49,7 @@ val replace_term_occ_modulo : occurrences or_like_first ->
val replace_term_occ_decl_modulo :
(occurrences * hyp_location_flag) or_like_first ->
'a testing_function -> (unit -> constr) ->
- named_declaration -> named_declaration
+ Context.Named.Declaration.t -> Context.Named.Declaration.t
(** [subst_closed_term_occ occl c d] replaces occurrences of
closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
@@ -62,7 +61,7 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
closed [c] at positions [occl] by [Rel 1] in [decl]. *)
val subst_closed_term_occ_decl : env -> evar_map ->
(occurrences * hyp_location_flag) or_like_first ->
- constr -> named_declaration -> named_declaration * evar_map
+ constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map
(** Miscellaneous *)
val error_invalid_occurrence : int list -> 'a
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 3f21842e3..40175dac9 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -19,7 +19,6 @@ open Globnames
open Nameops
open Term
open Vars
-open Context
open Namegen
open Declarations
open Declareops
@@ -61,7 +60,7 @@ let check_privacy_block mib =
let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in
- let indf = make_ind_family(pind, Context.extended_rel_list 0 lnamespar) in
+ let indf = make_ind_family(pind, Context.Rel.to_extended_list 0 lnamespar) in
let constrs = get_constructors env indf in
let projs = get_projections env indf in
@@ -92,8 +91,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
let pbody =
appvect
(mkRel (ndepar + nbprod),
- if dep then Context.extended_rel_vect 0 deparsign
- else Context.extended_rel_vect 1 arsign) in
+ if dep then Context.Rel.to_extended_vect 0 deparsign
+ else Context.Rel.to_extended_vect 1 arsign) in
let p =
it_mkLambda_or_LetIn_name env'
((if dep then mkLambda_name env' else mkLambda)
@@ -165,7 +164,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let base = applist (lift i pk,realargs) in
if depK then
Reduction.beta_appvect
- base [|applist (mkRel (i+1), Context.extended_rel_list 0 sign)|]
+ base [|applist (mkRel (i+1), Context.Rel.to_extended_list 0 sign)|]
else
base
| _ -> assert false
@@ -237,7 +236,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
| Ind _ ->
let realargs = List.skipn nparrec largs
- and arg = appvect (mkRel (i+1), Context.extended_rel_vect 0 hyps) in
+ and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in
applist(lift i fk,realargs@[arg])
| _ -> assert false
in
@@ -312,29 +311,29 @@ let mis_make_indrec env sigma listdepkind mib u =
(* arity in the context of the fixpoint, i.e.
P1..P_nrec f1..f_nbconstruct *)
- let args = Context.extended_rel_list (nrec+nbconstruct) lnamesparrec in
+ let args = Context.Rel.to_extended_list (nrec+nbconstruct) lnamesparrec in
let indf = make_ind_family((indi,u),args) in
let arsign,_ = get_arity env indf in
let depind = build_dependent_inductive env indf in
let deparsign = (Anonymous,None,depind)::arsign in
- let nonrecpar = rel_context_length lnonparrec in
- let larsign = rel_context_length deparsign in
+ let nonrecpar = Context.Rel.length lnonparrec in
+ let larsign = Context.Rel.length deparsign in
let ndepar = larsign - nonrecpar in
let dect = larsign+nrec+nbconstruct in
(* constructors in context of the Cases expr, i.e.
P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
- let args' = Context.extended_rel_list (dect+nrec) lnamesparrec in
- let args'' = Context.extended_rel_list ndepar lnonparrec in
+ let args' = Context.Rel.to_extended_list (dect+nrec) lnamesparrec in
+ let args'' = Context.Rel.to_extended_list ndepar lnonparrec in
let indf' = make_ind_family((indi,u),args'@args'') in
let branches =
let constrs = get_constructors env indf' in
let fi = Termops.rel_vect (dect-i-nctyi) nctyi in
let vecfi = Array.map
- (fun f -> appvect (f, Context.extended_rel_vect ndepar lnonparrec))
+ (fun f -> appvect (f, Context.Rel.to_extended_vect ndepar lnonparrec))
fi
in
Array.map3
@@ -355,9 +354,9 @@ let mis_make_indrec env sigma listdepkind mib u =
let deparsign' = (Anonymous,None,depind')::arsign' in
let pargs =
- let nrpar = Context.extended_rel_list (2*ndepar) lnonparrec
- and nrar = if dep then Context.extended_rel_list 0 deparsign'
- else Context.extended_rel_list 1 arsign'
+ let nrpar = Context.Rel.to_extended_list (2*ndepar) lnonparrec
+ and nrar = if dep then Context.Rel.to_extended_list 0 deparsign'
+ else Context.Rel.to_extended_list 1 arsign'
in nrpar@nrar
in
@@ -400,14 +399,14 @@ let mis_make_indrec env sigma listdepkind mib u =
let typtyi =
let concl =
- let pargs = if dep then Context.extended_rel_vect 0 deparsign
- else Context.extended_rel_vect 1 arsign
+ let pargs = if dep then Context.Rel.to_extended_vect 0 deparsign
+ else Context.Rel.to_extended_vect 1 arsign
in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
in it_mkProd_or_LetIn_name env
concl
deparsign
in
- mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp)
+ mrec (i+nctyi) (Context.Rel.nhyps arsign ::ln) (typtyi::ltyp)
(deftyi::ldef) rest
| [] ->
let fixn = Array.of_list (List.rev ln) in
@@ -428,7 +427,7 @@ let mis_make_indrec env sigma listdepkind mib u =
else
let recarg = (dest_subterms recargsvec.(tyi)).(j) in
let recarg = recargpar@recarg in
- let vargs = Context.extended_rel_list (nrec+i+j) lnamesparrec in
+ let vargs = Context.Rel.to_extended_list (nrec+i+j) lnamesparrec in
let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in
let p_0 =
type_rec_branch
@@ -442,7 +441,7 @@ let mis_make_indrec env sigma listdepkind mib u =
in
let rec put_arity env i = function
| ((indi,u),_,_,dep,kinds)::rest ->
- let indf = make_ind_family ((indi,u), Context.extended_rel_list i lnamesparrec) in
+ let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list i lnamesparrec) in
let s =
Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env)
evdref kinds
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index f429c51eb..1e3ff0fa2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -12,7 +12,6 @@ open Names
open Univ
open Term
open Vars
-open Context
open Termops
open Declarations
open Declareops
@@ -142,12 +141,12 @@ let constructor_nallargs_env env ((kn,i),j) =
let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *)
let (mib,mip) = Global.lookup_inductive indsp in
- mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+ mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt)
let constructor_nalldecls_env env ((kn,i),j) = (* TOCHANGE en decls *)
let mib = Environ.lookup_mind kn env in
let mip = mib.mind_packets.(i) in
- mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+ mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt)
(* Arity of constructors excluding params, excluding local defs *)
@@ -213,21 +212,21 @@ let inductive_nparams_env env ind =
let inductive_nparamdecls ind =
let (mib,mip) = Global.lookup_inductive ind in
- rel_context_length mib.mind_params_ctxt
+ Context.Rel.length mib.mind_params_ctxt
let inductive_nparamdecls_env env ind =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- rel_context_length mib.mind_params_ctxt
+ Context.Rel.length mib.mind_params_ctxt
(* Full length of arity (with local defs) *)
let inductive_nalldecls ind =
let (mib,mip) = Global.lookup_inductive ind in
- rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls
+ Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls
let inductive_nalldecls_env env ind =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls
+ Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls
(* Others *)
@@ -249,13 +248,13 @@ let inductive_alldecls_env env (ind,u) =
let constructor_has_local_defs (indsp,j) =
let (mib,mip) = Global.lookup_inductive indsp in
- let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) in
+ let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in
let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in
not (Int.equal l1 l2)
let inductive_has_local_defs ind =
let (mib,mip) = Global.lookup_inductive ind in
- let l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls in
+ let l1 = Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls in
let l2 = mib.mind_nparams + mip.mind_nrealargs in
not (Int.equal l1 l2)
@@ -273,11 +272,11 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
let make_case_info env ind style =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let ind_tags =
- rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
+ Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
let cstr_tags =
Array.map2 (fun c n ->
let d,_ = decompose_prod_assum c in
- rel_context_tags (List.firstn n d))
+ Context.Rel.to_tags (List.firstn n d))
mip.mind_nf_lc mip.mind_consnrealdecls in
let print_info = { ind_tags; cstr_tags; style } in
{ ci_ind = ind;
@@ -292,7 +291,7 @@ type constructor_summary = {
cs_cstr : pconstructor;
cs_params : constr list;
cs_nargs : int;
- cs_args : rel_context;
+ cs_args : Context.Rel.t;
cs_concl_realargs : constr array
}
@@ -306,10 +305,10 @@ let lift_constructor n cs = {
(* Accept either all parameters or only recursively uniform ones *)
let instantiate_params t params sign =
- let nnonrecpar = rel_context_nhyps sign - List.length params in
+ let nnonrecpar = Context.Rel.nhyps sign - List.length params in
(* Adjust the signature if recursively non-uniform parameters are not here *)
let _,sign = context_chop nnonrecpar sign in
- let _,t = decompose_prod_n_assum (rel_context_length sign) t in
+ let _,t = decompose_prod_n_assum (Context.Rel.length sign) t in
let subst = subst_of_rel_context_instance sign params in
substl subst t
@@ -323,7 +322,7 @@ let get_constructor ((ind,u as indu),mib,mip,params) j =
let vargs = List.skipn (List.length params) allargs in
{ cs_cstr = (ith_constructor_of_inductive ind j,u);
cs_params = params;
- cs_nargs = rel_context_length args;
+ cs_nargs = Context.Rel.length args;
cs_args = args;
cs_concl_realargs = Array.of_list vargs }
@@ -374,14 +373,14 @@ let build_dependent_constructor cs =
applist
(mkConstructU cs.cs_cstr,
(List.map (lift cs.cs_nargs) cs.cs_params)
- @(extended_rel_list 0 cs.cs_args))
+ @(Context.Rel.to_extended_list 0 cs.cs_args))
let build_dependent_inductive env ((ind, params) as indf) =
let arsign,_ = get_arity env indf in
let nrealargs = List.length arsign in
applist
(mkIndU ind,
- (List.map (lift nrealargs) params)@(extended_rel_list 0 arsign))
+ (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list 0 arsign))
(* builds the arity of an elimination predicate in sort [s] *)
@@ -506,7 +505,7 @@ let set_pattern_names env ind brv =
let arities =
Array.map
(fun c ->
- rel_context_length ((prod_assum c)) -
+ Context.Rel.length ((prod_assum c)) -
mib.mind_nparams)
mip.mind_nf_lc in
Array.map2 (set_names env) arities brv
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 9036f521e..42a00a7e2 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Declarations
open Environ
open Evd
@@ -92,12 +91,12 @@ val inductive_nparamdecls : inductive -> int
val inductive_nparamdecls_env : env -> inductive -> int
(** @return params context *)
-val inductive_paramdecls : pinductive -> rel_context
-val inductive_paramdecls_env : env -> pinductive -> rel_context
+val inductive_paramdecls : pinductive -> Context.Rel.t
+val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t
(** @return full arity context, hence with letin *)
-val inductive_alldecls : pinductive -> rel_context
-val inductive_alldecls_env : env -> pinductive -> rel_context
+val inductive_alldecls : pinductive -> Context.Rel.t
+val inductive_alldecls_env : env -> pinductive -> Context.Rel.t
(** {7 Extract information from a constructor name} *)
@@ -133,9 +132,9 @@ val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
type constructor_summary = {
cs_cstr : pconstructor; (* internal name of the constructor plus universes *)
- cs_params : constr list; (* parameters of the constructor in current ctx *)
- cs_nargs : int; (* length of arguments signature (letin included) *)
- cs_args : rel_context; (* signature of the arguments (letin included) *)
+ cs_params : constr list; (* parameters of the constructor in current ctx *)
+ cs_nargs : int; (* length of arguments signature (letin included) *)
+ cs_args : Context.Rel.t; (* signature of the arguments (letin included) *)
cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *)
}
val lift_constructor : int -> constructor_summary -> constructor_summary
@@ -148,11 +147,11 @@ val get_projections : env -> inductive_family -> constant array option
(** [get_arity] returns the arity of the inductive family instantiated
with the parameters; if recursively non-uniform parameters are not
part of the inductive family, they appears in the arity *)
-val get_arity : env -> inductive_family -> rel_context * sorts_family
+val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family
val build_dependent_constructor : constructor_summary -> constr
val build_dependent_inductive : env -> inductive_family -> constr
-val make_arity_signature : env -> bool -> inductive_family -> rel_context
+val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t
val make_arity : env -> bool -> inductive_family -> sorts -> types
val build_branch_type : env -> bool -> constr -> constructor_summary -> types
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7d5496917..84beaa9e3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,7 +28,6 @@ open Names
open Evd
open Term
open Vars
-open Context
open Termops
open Reductionops
open Environ
@@ -311,7 +310,7 @@ let ltac_interp_name_env k0 lvar env =
specification of pretype which accepts to start with a non empty
rel_context) *)
(* tail is the part of the env enriched by pretyping *)
- let n = rel_context_length (rel_context env) - k0 in
+ let n = Context.Rel.length (rel_context env) - k0 in
let ctxt,_ = List.chop n (rel_context env) in
let env = pop_rel_context n env in
let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in
@@ -515,14 +514,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
let ty' = pretype_type empty_valcon env evdref lvar ty in
let dcl = (na,None,ty'.utj_val) in
let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in
- type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl
+ type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl
| (na,bk,Some bd,ty)::bl ->
let ty' = pretype_type empty_valcon env evdref lvar ty in
let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in
- type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in
- let ctxtv = Array.map (type_bl env empty_rel_context) bl in
+ type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in
+ let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
let larj =
Array.map2
(fun e ar ->
@@ -549,7 +548,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
(* we lift nbfix times the type in tycon, because of
* the nbfix variables pushed to newenv *)
let (ctxt,ty) =
- decompose_prod_n_assum (rel_context_length ctxt)
+ decompose_prod_n_assum (Context.Rel.length ctxt)
(lift nbfix ftys.(i)) in
let nenv = push_rel_context ctxt newenv in
let j = pretype (mk_tycon ty) nenv evdref lvar def in
@@ -870,7 +869,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
let pred = nf_evar !evdref pred in
let p = nf_evar !evdref p in
let f cs b =
- let n = rel_context_length cs.cs_args in
+ let n = Context.Rel.length cs.cs_args in
let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist (pi, [build_dependent_constructor cs]) in
let csgn =
@@ -1003,7 +1002,7 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function
let ise_pretype_gen flags env sigma lvar kind c =
let evdref = ref sigma in
- let k0 = rel_context_length (rel_context env) in
+ let k0 = Context.Rel.length (rel_context env) in
let c' = match kind with
| WithoutTypeConstraint ->
(pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
@@ -1045,7 +1044,7 @@ let on_judgment f j =
let understand_judgment env sigma c =
let evdref = ref sigma in
- let k0 = rel_context_length (rel_context env) in
+ let k0 = Context.Rel.length (rel_context env) in
let j = pretype k0 true empty_tycon env evdref empty_lvar c in
let j = on_judgment (fun c ->
let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in
@@ -1053,7 +1052,7 @@ let understand_judgment env sigma c =
in j, Evd.evar_universe_context !evdref
let understand_judgment_tcc env evdref c =
- let k0 = rel_context_length (rel_context env) in
+ let k0 = Context.Rel.length (rel_context env) in
let j = pretype k0 true empty_tycon env evdref empty_lvar c in
on_judgment (fun c ->
let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3f02e4bfb..f59f88032 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -11,7 +11,6 @@ open Util
open Names
open Term
open Vars
-open Context
open Termops
open Univ
open Evd
@@ -1466,17 +1465,17 @@ let splay_prod_assum env sigma =
match kind_of_term t with
| Prod (x,t,c) ->
prodec_rec (push_rel (x,None,t) env)
- (add_rel_decl (x, None, t) l) c
+ (Context.Rel.add (x, None, t) l) c
| LetIn (x,b,t,c) ->
prodec_rec (push_rel (x, Some b, t) env)
- (add_rel_decl (x, Some b, t) l) c
+ (Context.Rel.add (x, Some b, t) l) c
| Cast (c,_,_) -> prodec_rec env l c
| _ ->
let t' = whd_betadeltaiota env sigma t in
if Term.eq_constr t t' then l,t
else prodec_rec env l t'
in
- prodec_rec env empty_rel_context
+ prodec_rec env Context.Rel.empty
let splay_arity env sigma c =
let l, c = splay_prod env sigma c in
@@ -1491,20 +1490,20 @@ let splay_prod_n env sigma n =
match kind_of_term (whd_betadeltaiota env sigma c) with
| Prod (n,a,c0) ->
decrec (push_rel (n,None,a) env)
- (m-1) (add_rel_decl (n,None,a) ln) c0
+ (m-1) (Context.Rel.add (n,None,a) ln) c0
| _ -> invalid_arg "splay_prod_n"
in
- decrec env n empty_rel_context
+ decrec env n Context.Rel.empty
let splay_lam_n env sigma n =
let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
match kind_of_term (whd_betadeltaiota env sigma c) with
| Lambda (n,a,c0) ->
decrec (push_rel (n,None,a) env)
- (m-1) (add_rel_decl (n,None,a) ln) c0
+ (m-1) (Context.Rel.add (n,None,a) ln) c0
| _ -> invalid_arg "splay_lam_n"
in
- decrec env n empty_rel_context
+ decrec env n Context.Rel.empty
let is_sort env sigma t =
match kind_of_term (whd_betadeltaiota env sigma t) with
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 30c7ded24..55bce2308 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Univ
open Evd
open Environ
@@ -218,10 +217,10 @@ val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr
val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr
val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts
val sort_of_arity : env -> evar_map -> constr -> sorts
-val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr
-val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr
+val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr
+val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr
val splay_prod_assum :
- env -> evar_map -> constr -> rel_context * constr
+ env -> evar_map -> constr -> Context.Rel.t * constr
type 'a miota_args = {
mP : constr; (** the result type *)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 89ba46dbc..70345c509 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -8,7 +8,6 @@
open Term
open Evd
-open Context
open Environ
(** This family of functions assumes its constr argument is known to be
@@ -44,6 +43,6 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
val type_of_global_reference_knowing_conclusion :
env -> evar_map -> constr -> types -> evar_map * types
-val sorts_of_context : env -> evar_map -> rel_context -> sorts list
+val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list
val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c44fbc0ba..5595c3cdc 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -12,7 +12,6 @@ open Globnames
open Decl_kinds
open Term
open Vars
-open Context
open Evd
open Util
open Typeclasses_errors
@@ -59,10 +58,10 @@ type typeclass = {
cl_impl : global_reference;
(* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
- cl_context : (global_reference * bool) option list * rel_context;
+ cl_context : (global_reference * bool) option list * Context.Rel.t;
(* Context of definitions and properties on defs, will not be shared *)
- cl_props : rel_context;
+ cl_props : Context.Rel.t;
(* The method implementaions as projections. *)
cl_projs : (Name.t * (direction * int option) option * constant option) list;
@@ -127,7 +126,7 @@ let typeclass_univ_instance (cl,u') =
in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst)
Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
in
- let subst_ctx = Context.map_rel_context (subst_univs_level_constr subst) in
+ let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in
{ cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context);
cl_props = subst_ctx cl.cl_props}, u'
@@ -204,7 +203,7 @@ let discharge_class (_,cl) =
(decl :: ctx', n :: subst)
) ctx ([], []) in
let discharge_rel_context subst n rel =
- let rel = map_rel_context (Cooking.expmod_constr repl) rel in
+ let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
let ctx, _ =
List.fold_right
(fun (id, b, t) (ctx, k) ->
@@ -287,7 +286,7 @@ let build_subclasses ~check env sigma glob pri =
| None -> []
| Some (rels, ((tc,u), args)) ->
let instapp =
- Reductionops.whd_beta sigma (appvectc c (Context.extended_rel_vect 0 rels))
+ Reductionops.whd_beta sigma (appvectc c (Context.Rel.to_extended_vect 0 rels))
in
let projargs = Array.of_list (args @ [instapp]) in
let projs = List.map_filter
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index b3170b970..f56af19a0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -9,7 +9,6 @@
open Names
open Globnames
open Term
-open Context
open Evd
open Environ
@@ -24,10 +23,10 @@ type typeclass = {
(** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
The boolean indicates if the typeclass argument is a direct superclass and the global reference
gives a direct link to the class itself. *)
- cl_context : (global_reference * bool) option list * rel_context;
+ cl_context : (global_reference * bool) option list * Context.Rel.t;
(** Context of definitions and properties on defs, will not be shared *)
- cl_props : rel_context;
+ cl_props : Context.Rel.t;
(** The methods implementations of the typeclass as projections.
Some may be undefinable due to sorting restrictions or simply undefined if
@@ -68,7 +67,7 @@ val dest_class_app : env -> constr -> typeclass puniverses * constr list
val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
(** Just return None if not a class *)
-val class_of_constr : constr -> (rel_context * (typeclass puniverses * constr list)) option
+val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option
val instance_impl : instance -> global_reference
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 585f066db..7a918ee87 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -9,7 +9,6 @@
(*i*)
open Names
open Term
-open Context
open Environ
open Constrexpr
open Globnames
@@ -20,7 +19,7 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
| UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *)
- | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
+ | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *)
exception TypeClassError of env * typeclass_error
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 7982fc852..b72d4db63 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -9,7 +9,6 @@
open Loc
open Names
open Term
-open Context
open Environ
open Constrexpr
open Globnames
@@ -19,7 +18,7 @@ type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
| UnboundMethod of global_reference * Id.t located (** Class name, method *)
- | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
+ | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *)
exception TypeClassError of env * typeclass_error
@@ -27,5 +26,5 @@ val not_a_class : env -> constr -> 'a
val unbound_method : env -> global_reference -> Id.t located -> 'a
-val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
+val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e8a0df484..b42a70b34 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1582,7 +1582,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
| AllOccurrences, InHyp as occ ->
let occ = if likefirst then LikeFirst else AtOccs occ in
let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
- if Context.eq_named_declaration d newdecl
+ if Context.Named.Declaration.equal d newdecl
&& not (indirectly_dependent c d depdecls)
then
if check_occs && not (in_every_hyp occs)
@@ -1634,7 +1634,7 @@ type abstraction_request =
type 'r abstraction_result =
Names.Id.t * named_context_val *
- Context.named_declaration list * Names.Id.t option *
+ Context.Named.Declaration.t list * Names.Id.t option *
types * (constr, 'r) Sigma.sigma option
let make_abstraction env evd ccl abs =
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 51a51f375..14bcb4a06 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -77,7 +77,7 @@ val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
type 'r abstraction_result =
Names.Id.t * named_context_val *
- Context.named_declaration list * Names.Id.t option *
+ Context.Named.Declaration.t list * Names.Id.t option *
types * (constr, 'r) Sigma.sigma option
val make_abstraction : env -> 'r Sigma.t -> constr ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c59e085e5..38eea9170 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -53,7 +53,7 @@ let type_constructor mind mib u typ params =
let s = ind_subst mind mib u in
let ctyp = substl s typ in
let ctyp = subst_instance_constr u ctyp in
- let ndecls = Context.rel_context_length mib.mind_params_ctxt in
+ let ndecls = Context.Rel.length mib.mind_params_ctxt in
if Int.equal ndecls 0 then ctyp
else
let _,ctyp = decompose_prod_n_assum ndecls ctyp in
diff --git a/printing/printer.ml b/printing/printer.ml
index b6dda93c2..08fd0186a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -293,7 +293,7 @@ let pr_named_context_of env sigma =
hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
let pr_named_context env sigma ne_context =
- hv 0 (Context.fold_named_context
+ hv 0 (Context.Named.fold_outside
(fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d)
ne_context ~init:(mt ()))
@@ -306,7 +306,7 @@ 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.fold_named_list_context
+ Context.NamedList.fold
(fun d pps ->
let pidt = pr_var_list_decl env sigma d in
(pps ++ fnl () ++ pidt))
@@ -333,7 +333,7 @@ let pr_context_limit n env sigma =
else
let k = lgsign-n in
let _,sign_env =
- Context.fold_named_list_context
+ Context.NamedList.fold
(fun d (i,pps) ->
if i < k then
(i+1, (pps ++str "."))
@@ -726,7 +726,7 @@ let prterm = pr_lconstr
type context_object =
| Variable of Id.t (* A section variable or a Let definition *)
- | Axiom of constant * (Label.t * Context.rel_context * types) list
+ | Axiom of constant * (Label.t * Context.Rel.t * types) list
| Opaque of constant (* An opaque constant. *)
| Transparent of constant
diff --git a/printing/printer.mli b/printing/printer.mli
index 5c60b8936..bdb295a47 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -10,7 +10,6 @@ open Pp
open Names
open Globnames
open Term
-open Context
open Environ
open Pattern
open Evd
@@ -109,13 +108,13 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds
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 -> named_declaration -> std_ppcmds
-val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds
-val pr_rel_decl : env -> evar_map -> rel_declaration -> 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_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
-val pr_named_context : env -> evar_map -> named_context -> std_ppcmds
+val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds
val pr_named_context_of : env -> evar_map -> std_ppcmds
-val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds
+val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds
val pr_rel_context_of : env -> evar_map -> std_ppcmds
val pr_context_of : env -> evar_map -> std_ppcmds
@@ -165,7 +164,7 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *)
type context_object =
| Variable of Id.t (** A section variable or a Let definition *)
(** An axiom and the type it inhabits (if an axiom of the empty type) *)
- | Axiom of constant * (Label.t * Context.rel_context * types) list
+ | Axiom of constant * (Label.t * Context.Rel.t * types) list
| Opaque of constant (** An opaque constant. *)
| Transparent of constant (** A transparent constant *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index e0b1d55be..3973c2db6 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -65,7 +65,6 @@ let get_new_id locals id =
(** Inductive declarations *)
-open Context
open Termops
open Reduction
@@ -90,7 +89,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = extended_rel_list 0 params in
+ let args = Context.Rel.to_extended_list 0 params in
let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
@@ -144,7 +143,7 @@ let print_record env mind mib =
in
let mip = mib.mind_packets.(0) in
let params = Inductive.inductive_paramdecls (mib,u) in
- let args = extended_rel_list 0 params in
+ let args = Context.Rel.to_extended_list 0 params in
let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index a00a95a2f..46318b789 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -67,7 +67,7 @@ module V82 : sig
val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
(* Used for congruence closure *)
- val new_goal_with : Evd.evar_map -> goal -> Context.named_context -> goal Evd.sigma
+ val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma
(* Used by the compatibility layer and typeclasses *)
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 1ba14e7d4..e80f5a64c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -13,7 +13,6 @@ open Names
open Nameops
open Term
open Vars
-open Context
open Termops
open Environ
open Reductionops
diff --git a/proofs/logic.mli b/proofs/logic.mli
index d034b73c5..d33f56bb7 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -53,4 +53,4 @@ exception RefinerError of refiner_error
val catchable_exception : exn -> bool
val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
- Context.named_declaration -> Environ.named_context_val
+ Context.Named.Declaration.t -> Environ.named_context_val
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9f2a00135..155b2cfca 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -215,7 +215,7 @@ let solve_by_implicit_tactic env sigma evk =
match (!implicit_tactic, snd (evar_source evk sigma)) with
| Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
when
- Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
+ Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
(try
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 96fe474f6..1c968e427 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -446,7 +446,7 @@ module Goal : sig
environment of [gl] (i.e. the global environment and the
hypotheses) and the current evar map. *)
val concl : ([ `NF ], 'r) t -> Term.constr
- val hyps : ([ `NF ], 'r) t -> Context.named_context
+ val hyps : ([ `NF ], 'r) t -> Context.Named.t
val env : ('a, 'r) t -> Environ.env
val sigma : ('a, 'r) t -> 'r Sigma.t
val extra : ('a, 'r) t -> Evd.Store.t
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ba62b2cb2..de7025062 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -197,10 +197,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
destruct), this is not detected by this tactical. *)
let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
:Proof_type.goal list Evd.sigma =
- let oldhyps:Context.named_context = pf_hyps goal in
+ let oldhyps:Context.Named.t = pf_hyps goal in
let rslt:Proof_type.goal list Evd.sigma = tac goal in
let { it = gls; sigma = sigma; } = rslt in
- let hyps:Context.named_context list =
+ let hyps:Context.Named.t list =
List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in
let newhyps =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index a81555ff5..2959787d4 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Context
open Evd
open Proof_type
@@ -16,7 +15,7 @@ val sig_it : 'a sigma -> 'a
val project : 'a sigma -> evar_map
val pf_env : goal sigma -> Environ.env
-val pf_hyps : goal sigma -> named_context
+val pf_hyps : goal sigma -> Context.Named.t
val unpackage : 'a sigma -> evar_map ref * 'a
val repackage : evar_map ref -> 'a -> 'a sigma
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 57c60cbee..dc0cf81a7 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -48,7 +48,7 @@ let pf_last_hyp gl = List.hd (pf_hyps gl)
let pf_get_hyp gls id =
try
- Context.lookup_named id (pf_hyps gls)
+ Context.Named.lookup id (pf_hyps gls)
with Not_found ->
raise (RefinerError (NoSuchHyp id))
@@ -198,7 +198,7 @@ module New = struct
let pf_get_hyp id gl =
let hyps = Proofview.Goal.hyps gl in
let sign =
- try Context.lookup_named id hyps
+ try Context.Named.lookup id hyps
with Not_found -> raise (RefinerError (NoSuchHyp id))
in
sign
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index c45fd250c..b7915e837 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Environ
open Evd
open Proof_type
@@ -34,18 +33,18 @@ val apply_sig_tac :
val pf_concl : goal sigma -> types
val pf_env : goal sigma -> env
-val pf_hyps : goal sigma -> named_context
+val pf_hyps : goal sigma -> Context.Named.t
(*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*)
val pf_hyps_types : goal sigma -> (Id.t * types) list
val pf_nth_hyp_id : goal sigma -> int -> Id.t
-val pf_last_hyp : goal sigma -> named_declaration
+val pf_last_hyp : goal sigma -> Context.Named.Declaration.t
val pf_ids_of_hyps : goal sigma -> Id.t list
val pf_global : goal sigma -> Id.t -> constr
val pf_unsafe_type_of : goal sigma -> constr -> types
val pf_type_of : goal sigma -> constr -> evar_map * types
val pf_hnf_type_of : goal sigma -> constr -> types
-val pf_get_hyp : goal sigma -> Id.t -> named_declaration
+val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t
val pf_get_hyp_typ : goal sigma -> Id.t -> types
val pf_get_new_id : Id.t -> goal sigma -> Id.t
@@ -123,9 +122,9 @@ module New : sig
val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list
- val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration
+ val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
- val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration
+ val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types
diff --git a/tactics/auto.ml b/tactics/auto.ml
index d6552920f..726422c6f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -321,7 +321,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
let env = Proofview.Goal.env gl in
let nf c = Evarutil.nf_evar sigma c in
let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
- let hyp = Context.map_named_declaration nf decl in
+ let hyp = Context.Named.Declaration.map nf decl in
let hintl = make_resolve_hyp env sigma hyp
in trivial_fail_db dbg mod_delta db_list
(Hint_db.add_list env sigma hintl local_db)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 64a68ba6b..2c713a021 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -49,7 +49,6 @@ open Util
open Names
open Term
open Vars
-open Context
open Declarations
open Environ
open Inductive
@@ -71,8 +70,8 @@ let build_dependent_inductive ind (mib,mip) =
let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
applist
(mkIndU ind,
- extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt
- @ extended_rel_list 0 realargs)
+ Context.Rel.to_extended_list mip.mind_nrealdecls mib.mind_params_ctxt
+ @ Context.Rel.to_extended_list 0 realargs)
let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s
@@ -109,7 +108,7 @@ let get_sym_eq_data env (ind,u) =
error "Inductive equalities with local definitions in arity not supported.";
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
- if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
+ if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
error "Constructor must have no arguments"; (* This can be relaxed... *)
let params,constrargs = List.chop mib.mind_nparams constrargs in
if mip.mind_nrealargs > mib.mind_nparams then
@@ -144,7 +143,7 @@ let get_non_sym_eq_data env (ind,u) =
error "Inductive equalities with local definitions in arity not supported";
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
- if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
+ if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
error "Constructor must have no arguments";
let _,constrargs = List.chop mib.mind_nparams constrargs in
let constrargs = List.map (Vars.subst_instance_constr u) constrargs in
@@ -170,7 +169,7 @@ let build_sym_scheme env ind =
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env indu in
let cstr n =
- mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
+ mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
let applied_ind = build_dependent_inductive indu specif in
let realsign_ind =
@@ -183,7 +182,7 @@ let build_sym_scheme env ind =
my_it_mkLambda_or_LetIn_name
(lift_rel_context (nrealargs+1) realsign_ind)
(mkApp (mkIndU indu,Array.concat
- [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+ [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
rel_vect 1 nrealargs;
rel_vect (2*nrealargs+2) nrealargs])),
mkRel 1 (* varH *),
@@ -224,13 +223,13 @@ let build_sym_involutive_scheme env ind =
get_sym_eq_data env indu in
let eq,eqrefl,ctx = get_coq_eq ctx in
let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
- let cstr n = mkApp (mkConstructUi (indu,1),extended_rel_vect n paramsctxt) in
+ let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect n paramsctxt) in
let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
let applied_ind = build_dependent_inductive indu specif in
let applied_ind_C =
mkApp
(mkIndU indu, Array.append
- (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt)
+ (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt)
(rel_vect (nrealargs+1) nrealargs)) in
let realsign_ind =
name_context env ((Name varH,None,applied_ind)::realsign) in
@@ -244,15 +243,15 @@ let build_sym_involutive_scheme env ind =
(mkApp (eq,[|
mkApp
(mkIndU indu, Array.concat
- [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+ [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
rel_vect (2*nrealargs+2) nrealargs;
rel_vect 1 nrealargs]);
mkApp (sym,Array.concat
- [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+ [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
rel_vect 1 nrealargs;
rel_vect (2*nrealargs+2) nrealargs;
[|mkApp (sym,Array.concat
- [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+ [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
rel_vect (2*nrealargs+2) nrealargs;
rel_vect 1 nrealargs;
[|mkRel 1|]])|]]);
@@ -335,7 +334,7 @@ let build_l2r_rew_scheme dep env ind kind =
let eq,eqrefl,ctx = get_coq_eq ctx in
let cstr n p =
mkApp (mkConstructUi(indu,1),
- Array.concat [extended_rel_vect n paramsctxt1;
+ Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
rel_vect p nrealargs]) in
let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
let varHC = fresh env (Id.of_string "HC") in
@@ -343,12 +342,12 @@ let build_l2r_rew_scheme dep env ind kind =
let applied_ind = build_dependent_inductive indu specif in
let applied_ind_P =
mkApp (mkIndU indu, Array.concat
- [extended_rel_vect (3*nrealargs) paramsctxt1;
+ [Context.Rel.to_extended_vect (3*nrealargs) paramsctxt1;
rel_vect 0 nrealargs;
rel_vect nrealargs nrealargs]) in
let applied_ind_G =
mkApp (mkIndU indu, Array.concat
- [extended_rel_vect (3*nrealargs+3) paramsctxt1;
+ [Context.Rel.to_extended_vect (3*nrealargs+3) paramsctxt1;
rel_vect (nrealargs+3) nrealargs;
rel_vect 0 nrealargs]) in
let realsign_P = lift_rel_context nrealargs realsign in
@@ -359,10 +358,10 @@ let build_l2r_rew_scheme dep env ind kind =
lift_rel_context (nrealargs+3) realsign) in
let applied_sym_C n =
mkApp(sym,
- Array.append (extended_rel_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
+ Array.append (Context.Rel.to_extended_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
let applied_sym_G =
mkApp(sym,
- Array.concat [extended_rel_vect (nrealargs*3+4) paramsctxt1;
+ Array.concat [Context.Rel.to_extended_vect (nrealargs*3+4) paramsctxt1;
rel_vect (nrealargs+4) nrealargs;
rel_vect 1 nrealargs;
[|mkRel 1|]]) in
@@ -372,7 +371,7 @@ let build_l2r_rew_scheme dep env ind kind =
let ci = make_case_info (Global.env()) ind RegularStyle in
let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in
let applied_PC =
- mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign)
+ mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect 1 realsign)
(if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
let applied_PG =
mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs)
@@ -382,11 +381,11 @@ let build_l2r_rew_scheme dep env ind kind =
(if dep then [|mkRel 2|] else [||])) in
let applied_sym_sym =
mkApp (sym,Array.concat
- [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+ [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
rel_vect 4 nrealargs;
rel_vect (nrealargs+4) nrealargs;
[|mkApp (sym,Array.concat
- [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+ [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
rel_vect (nrealargs+4) nrealargs;
rel_vect 4 nrealargs;
[|mkRel 2|]])|]]) in
@@ -409,7 +408,7 @@ let build_l2r_rew_scheme dep env ind kind =
mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
applied_PR)),
mkApp (sym_involutive,
- Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
+ Array.append (Context.Rel.to_extended_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
[|main_body|])
else
main_body))))))
@@ -448,7 +447,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
get_sym_eq_data env indu in
let cstr n p =
mkApp (mkConstructUi(indu,1),
- Array.concat [extended_rel_vect n paramsctxt1;
+ Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
rel_vect p nrealargs]) in
let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
let varHC = fresh env (Id.of_string "HC") in
@@ -456,12 +455,12 @@ let build_l2r_forward_rew_scheme dep env ind kind =
let applied_ind = build_dependent_inductive indu specif in
let applied_ind_P =
mkApp (mkIndU indu, Array.concat
- [extended_rel_vect (4*nrealargs+2) paramsctxt1;
+ [Context.Rel.to_extended_vect (4*nrealargs+2) paramsctxt1;
rel_vect 0 nrealargs;
rel_vect (nrealargs+1) nrealargs]) in
let applied_ind_P' =
mkApp (mkIndU indu, Array.concat
- [extended_rel_vect (3*nrealargs+1) paramsctxt1;
+ [Context.Rel.to_extended_vect (3*nrealargs+1) paramsctxt1;
rel_vect 0 nrealargs;
rel_vect (2*nrealargs+1) nrealargs]) in
let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
@@ -539,7 +538,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
get_non_sym_eq_data env indu in
let cstr n =
- mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
+ mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
let constrargs_cstr = constrargs@[cstr 0] in
let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
let varHC = fresh env (Id.of_string "HC") in
@@ -555,8 +554,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
let applied_PG =
mkApp (mkVar varP,
- if dep then extended_rel_vect 0 realsign_ind
- else extended_rel_vect 1 realsign) in
+ if dep then Context.Rel.to_extended_vect 0 realsign_ind
+ else Context.Rel.to_extended_vect 1 realsign) in
let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign_ind
@@ -600,12 +599,12 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
| hp :: p :: ind :: indargs ->
let c' =
my_it_mkLambda_or_LetIn indargs
- (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p)
- (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp)
- (mkLambda_or_LetIn (map_rel_declaration (lift 2) ind)
+ (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 1) p)
+ (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 2) hp)
+ (mkLambda_or_LetIn (Context.Rel.Declaration.map (lift 2) ind)
(Reductionops.whd_beta Evd.empty
(applist (c,
- extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
+ Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
in c', ctx'
| _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
@@ -744,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind =
let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
- if Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then
+ if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then
error "Constructor must have no arguments";
let b = List.nth constrargs (i + mib.mind_nparams - 1) in
let varB = fresh env (Id.of_string "B") in
@@ -760,8 +759,8 @@ let build_congr env (eq,refl,ctx) ind =
(mkNamedLambda varH
(applist
(mkIndU indu,
- extended_rel_list (mip.mind_nrealargs+2) paramsctxt @
- extended_rel_list 0 realsign))
+ Context.Rel.to_extended_list (mip.mind_nrealargs+2) paramsctxt @
+ Context.Rel.to_extended_list 0 realsign))
(mkCase (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (mip.mind_nrealargs+3) realsign)
@@ -769,9 +768,9 @@ let build_congr env (eq,refl,ctx) ind =
(Anonymous,
applist
(mkIndU indu,
- extended_rel_list (2*mip.mind_nrealdecls+3)
+ Context.Rel.to_extended_list (2*mip.mind_nrealdecls+3)
paramsctxt
- @ extended_rel_list 0 realsign),
+ @ Context.Rel.to_extended_list 0 realsign),
mkApp (eq,
[|mkVar varB;
mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1854b4120..ac41c9464 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1574,7 +1574,7 @@ let unfold_body x =
Proofview.Goal.enter { enter = begin fun gl ->
(** We normalize the given hypothesis immediately. *)
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
- let (_, xval, _) = Context.lookup_named x hyps in
+ let (_, xval, _) = Context.Named.lookup x hyps in
let xval = match xval with
| None -> errorlabstrm "unfold_body"
(pr_id x ++ str" is not a defined hypothesis.")
@@ -1656,7 +1656,7 @@ let subst_one_var dep_proof_ok x =
(** [is_eq_x] ensures nf_evar on its side *)
let hyps = Proofview.Goal.hyps gl in
let test hyp _ = is_eq_x gl varx hyp in
- Context.fold_named_context test ~init:() hyps;
+ Context.Named.fold_outside test ~init:() hyps;
errorlabstrm "Subst"
(str "Cannot find any non-recursive equality over " ++ pr_id x ++
str".")
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a957a5624..15765bab5 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -323,7 +323,7 @@ let project_hint pri l2r r =
| _ -> assert false in
let p =
if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
- let c = Reductionops.whd_beta Evd.empty (mkApp (c,Context.extended_rel_vect 0 sign)) in
+ let c = Reductionops.whd_beta Evd.empty (mkApp (c, Context.Rel.to_extended_vect 0 sign)) in
let c = it_mkLambda_or_LetIn
(mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
let id =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 257598d18..c9187f54a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -10,7 +10,6 @@ open Pp
open Util
open Names
open Term
-open Context
open Environ
open Globnames
open Decl_kinds
@@ -192,7 +191,7 @@ val make_resolves :
If the hyp cannot be used as a Hint, the empty list is returned. *)
val make_resolve_hyp :
- env -> evar_map -> named_declaration -> hint_entry list
+ env -> evar_map -> Context.Named.Declaration.t -> hint_entry list
(** [make_extern pri pattern tactic_expr] *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ed1a62795..3574990f6 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,7 +13,6 @@ open Names
open Nameops
open Term
open Vars
-open Context
open Termops
open Namegen
open Environ
@@ -97,7 +96,7 @@ let make_inv_predicate env evd indf realargs id status concl =
(* We lift to make room for the equations *)
(hyps,lift nrealargs bodypred)
in
- let nhyps = rel_context_length hyps in
+ let nhyps = Context.Rel.length hyps in
let env' = push_rel_context hyps env in
(* Now the arity is pushed, and we need to construct the pairs
* ai,mkRel(n-i+1) *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 75e69bc09..9154c50c8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -14,7 +14,6 @@ open Term
open Vars
open Termops
open Namegen
-open Context
open Evd
open Printer
open Reductionops
@@ -157,7 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
fold_named_context
(fun env (id,_,_ as d) (revargs,hyps) ->
if Id.List.mem id ivars then
- ((mkVar id)::revargs,add_named_decl d hyps)
+ ((mkVar id)::revargs, Context.Named.add d hyps)
else
(revargs,hyps))
env ~init:([],[])
@@ -206,8 +205,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
fold_named_context
(fun env (id,_,_ as d) sign ->
if mem_named_context id global_named_context then sign
- else add_named_decl d sign)
- invEnv ~init:empty_named_context
+ else Context.Named.add d sign)
+ invEnv ~init:Context.Named.empty
end in
let avoid = ref [] in
let { sigma=sigma } = Proof.V82.subgoals pf in
@@ -218,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let h = next_ident_away (Id.of_string "H") !avoid in
let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
avoid := h::!avoid;
- ownSign := add_named_decl (h,None,ty) !ownSign;
+ ownSign := Context.Named.add (h,None,ty) !ownSign;
applist (mkVar h, inst)
| _ -> map_constr fill_holes c
in
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 40a18ac45..1de47b2be 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -71,7 +71,7 @@ val cl_rewrite_clause :
bool -> Locus.occurrences -> Id.t option -> tactic
val is_applied_rewrite_relation :
- env -> evar_map -> Context.rel_context -> constr -> types option
+ env -> evar_map -> Context.Rel.t -> constr -> types option
val declare_relation :
?binders:local_binder list -> constr_expr -> constr_expr -> Id.t ->
diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli
index d8e6dd0ae..090207bcc 100644
--- a/tactics/tactic_matching.mli
+++ b/tactics/tactic_matching.mli
@@ -43,7 +43,7 @@ val match_term :
val match_goal:
Environ.env ->
Evd.evar_map ->
- Context.named_context ->
+ Context.Named.t ->
Term.constr ->
(Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
Tacexpr.glob_tactic_expr t Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 74714300c..750ec8fb1 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -12,7 +12,6 @@ open Util
open Names
open Term
open Termops
-open Context
open Declarations
open Tacmach
open Clenv
@@ -154,8 +153,8 @@ type branch_args = {
branchnames : Tacexpr.intro_patterns}
type branch_assumptions = {
- ba : branch_args; (* the branch args *)
- assums : named_context} (* the list of assumptions introduced *)
+ ba : branch_args; (* the branch args *)
+ assums : Context.Named.t} (* the list of assumptions introduced *)
let fix_empty_or_and_pattern nv l =
(* 1- The syntax does not distinguish between "[ ]" for one clause with no
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 042f80fe8..147f1f0f2 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -9,7 +9,6 @@
open Pp
open Names
open Term
-open Context
open Tacmach
open Proof_type
open Tacexpr
@@ -60,29 +59,29 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
val onNthHypId : int -> (Id.t -> tactic) -> tactic
val onNthHyp : int -> (constr -> tactic) -> tactic
-val onNthDecl : int -> (named_declaration -> tactic) -> tactic
+val onNthDecl : int -> (Context.Named.Declaration.t -> tactic) -> tactic
val onLastHypId : (Id.t -> tactic) -> tactic
val onLastHyp : (constr -> tactic) -> tactic
-val onLastDecl : (named_declaration -> tactic) -> tactic
+val onLastDecl : (Context.Named.Declaration.t -> tactic) -> tactic
val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic
val onNLastHyps : int -> (constr list -> tactic) -> tactic
-val onNLastDecls : int -> (named_context -> tactic) -> tactic
+val onNLastDecls : int -> (Context.Named.t -> tactic) -> tactic
val lastHypId : goal sigma -> Id.t
val lastHyp : goal sigma -> constr
-val lastDecl : goal sigma -> named_declaration
+val lastDecl : goal sigma -> Context.Named.Declaration.t
val nLastHypsId : int -> goal sigma -> Id.t list
val nLastHyps : int -> goal sigma -> constr list
-val nLastDecls : int -> goal sigma -> named_context
+val nLastDecls : int -> goal sigma -> Context.Named.t
-val afterHyp : Id.t -> goal sigma -> named_context
+val afterHyp : Id.t -> goal sigma -> Context.Named.t
val ifOnHyp : (Id.t * types -> bool) ->
(Id.t -> tactic) -> (Id.t -> tactic) ->
Id.t -> tactic
-val onHyps : (goal sigma -> named_context) ->
- (named_context -> tactic) -> tactic
+val onHyps : (goal sigma -> Context.Named.t) ->
+ (Context.Named.t -> tactic) -> tactic
(** {6 Tacticals applying to goal components } *)
@@ -99,18 +98,18 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic
(** {6 Elimination tacticals. } *)
type branch_args = {
- ity : pinductive; (** the type we were eliminating on *)
+ ity : pinductive; (** the type we were eliminating on *)
largs : constr list; (** its arguments *)
branchnum : int; (** the branch number *)
pred : constr; (** the predicate we used *)
nassums : int; (** the number of assumptions to be introduced *)
branchsign : bool list; (** the signature of the branch.
- true=recursive argument, false=constant *)
+ true=recursive argument, false=constant *)
branchnames : intro_patterns}
type branch_assumptions = {
- ba : branch_args; (** the branch args *)
- assums : named_context} (** the list of assumptions introduced *)
+ ba : branch_args; (** the branch args *)
+ assums : Context.Named.t} (** the list of assumptions introduced *)
(** [check_disjunctive_pattern_size loc pats n] returns an appropriate
error message if |pats| <> n *)
@@ -224,7 +223,7 @@ module New : sig
val tclTIMEOUT : int -> unit tactic -> unit tactic
val tclTIME : string option -> 'a tactic -> 'a tactic
- val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context
+ val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t
val ifOnHyp : (identifier * types -> bool) ->
(identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
@@ -233,11 +232,11 @@ module New : sig
val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic
val onLastHypId : (identifier -> unit tactic) -> unit tactic
val onLastHyp : (constr -> unit tactic) -> unit tactic
- val onLastDecl : (named_declaration -> unit tactic) -> unit tactic
+ val onLastDecl : (Context.Named.Declaration.t -> unit tactic) -> unit tactic
- val onHyps : ([ `NF ], named_context) Proofview.Goal.enter ->
- (named_context -> unit tactic) -> unit tactic
- val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic
+ val onHyps : ([ `NF ], Context.Named.t) Proofview.Goal.enter ->
+ (Context.Named.t -> unit tactic) -> unit tactic
+ val afterHyp : Id.t -> (Context.Named.t -> unit tactic) -> unit tactic
val tryAllHyps : (identifier -> unit tactic) -> unit tactic
val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1349d5517..588bdc8ed 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -13,7 +13,6 @@ open Names
open Nameops
open Term
open Vars
-open Context
open Termops
open Find_subterm
open Namegen
@@ -1405,7 +1404,7 @@ let make_projection env sigma params cstr sign elim i n c u =
then
let t = lift (i+1-n) t in
let abselim = beta_applist (elim,params@[t;branch]) in
- let c = beta_applist (abselim, [mkApp (c, extended_rel_vect 0 sign)]) in
+ let c = beta_applist (abselim, [mkApp (c, Context.Rel.to_extended_vect 0 sign)]) in
Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
else
None
@@ -1413,7 +1412,7 @@ let make_projection env sigma params cstr sign elim i n c u =
(* goes from left to right when i increases! *)
match List.nth l i with
| Some proj ->
- let args = extended_rel_vect 0 sign in
+ let args = Context.Rel.to_extended_vect 0 sign in
let proj =
if Environ.is_projection proj env then
mkProj (Projection.make proj false, mkApp (c, args))
@@ -1942,7 +1941,7 @@ let bring_hyps hyps =
let store = Proofview.Goal.extra gl in
let concl = Tacmach.New.pf_nf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
- let args = Array.of_list (instance_from_named_context hyps) in
+ let args = Array.of_list (Context.Named.to_instance hyps) in
Proofview.Refine.refine { run = begin fun sigma ->
let Sigma (ev, sigma, p) =
Evarutil.new_evar env sigma ~principal:true ~store newcl in
@@ -2568,7 +2567,7 @@ let generalize_dep ?(with_let=false) c gl =
d::toquant
else
toquant in
- let to_quantify = Context.fold_named_context seek sign ~init:[] in
+ let to_quantify = Context.Named.fold_outside seek sign ~init:[] in
let to_quantify_rev = List.rev to_quantify in
let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in
let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
@@ -2588,7 +2587,7 @@ let generalize_dep ?(with_let=false) c gl =
in
let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
(cl',project gl) in
- let args = instance_from_named_context to_quantify_rev in
+ let args = Context.Named.to_instance to_quantify_rev in
tclTHENLIST
[tclEVARS evd;
Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args));
@@ -2710,7 +2709,7 @@ let specialize (c,lbind) =
let unfold_body x gl =
let hyps = pf_hyps gl in
let xval =
- match Context.lookup_named x hyps with
+ match Context.Named.lookup x hyps with
(_,Some xval,_) -> xval
| _ -> errorlabstrm "unfold_body"
(pr_id x ++ str" is not a defined hypothesis.") in
@@ -3131,20 +3130,20 @@ type elim_scheme = {
elimc: constr with_bindings option;
elimt: types;
indref: global_reference option;
- params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
- nparams: int; (* number of parameters *)
- predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
- npredicates: int; (* Number of predicates *)
- branches: rel_context; (* branchr,...,branch1 *)
- nbranches: int; (* Number of branches *)
- args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *)
- nargs: int; (* number of arguments *)
- indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni)
- if HI is in premisses, None otherwise *)
- concl: types; (* Qi x1...xni HI (f...), HI and (f...)
- are optional and mutually exclusive *)
- indarg_in_concl: bool; (* true if HI appears at the end of conclusion *)
- farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *)
+ params: Context.Rel.t; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+ nparams: int; (* number of parameters *)
+ predicates: Context.Rel.t; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+ npredicates: int; (* Number of predicates *)
+ branches: Context.Rel.t; (* branchr,...,branch1 *)
+ nbranches: int; (* Number of branches *)
+ args: Context.Rel.t; (* (xni, Ti_ni) ... (x1, Ti_1) *)
+ nargs: int; (* number of arguments *)
+ indarg: Context.Rel.Declaration.t option; (* Some (H,I prm1..prmp x1...xni)
+ if HI is in premisses, None otherwise *)
+ concl: types; (* Qi x1...xni HI (f...), HI and (f...)
+ are optional and mutually exclusive *)
+ indarg_in_concl: bool; (* true if HI appears at the end of conclusion *)
+ farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *)
}
let empty_scheme =
@@ -3303,7 +3302,7 @@ let hyps_of_vars env sign nogen hyps =
if Id.Set.is_empty hyps then []
else
let (_,lh) =
- Context.fold_named_context_reverse
+ Context.Named.fold_inside
(fun (hs,hl) (x,_,_ as d) ->
if Id.Set.mem x nogen then (hs,hl)
else if Id.Set.mem x hs then (hs,x::hl)
@@ -3534,7 +3533,7 @@ let occur_rel n c =
We also return the conclusion.
*)
let decompose_paramspred_branch_args elimt =
- let rec cut_noccur elimt acc2 : rel_context * rel_context * types =
+ let rec cut_noccur elimt acc2 : Context.Rel.t * Context.Rel.t * types =
match kind_of_term elimt with
| Prod(nme,tpe,elimt') ->
let hd_tpe,_ = decompose_app ((strip_prod_assum tpe)) in
@@ -3543,7 +3542,7 @@ let decompose_paramspred_branch_args elimt =
else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl
| App(_, _) | Rel _ -> acc2 , [] , elimt
| _ -> error_ind_scheme "" in
- let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types =
+ let rec cut_occur elimt acc1 : Context.Rel.t * Context.Rel.t * Context.Rel.t * types =
match kind_of_term elimt with
| Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1)
| Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl
@@ -3671,7 +3670,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
let ind_is_ok =
List.equal Term.eq_constr
(List.lastn scheme.nargs indargs)
- (extended_rel_list 0 scheme.args) in
+ (Context.Rel.to_extended_list 0 scheme.args) in
if not (ccl_arg_ok && ind_is_ok) then
error_ind_scheme "the conclusion of"
in (cond, check_concl)
@@ -4586,10 +4585,10 @@ let abstract_subproof id gk tac =
List.fold_right
(fun (id,_,_ as d) (s1,s2) ->
if mem_named_context id current_sign &&
- interpretable_as_section_decl evdref (Context.lookup_named id current_sign) d
+ interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d
then (s1,push_named_context_val d s2)
- else (add_named_decl d s1,s2))
- global_sign (empty_named_context,empty_named_context_val) in
+ else (Context.Named.add d s1,s2))
+ global_sign (Context.Named.empty, empty_named_context_val) in
let id = next_global_ident_away id (pf_ids_of_hyps gl) in
let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
let concl =
@@ -4617,7 +4616,7 @@ let abstract_subproof id gk tac =
in
let const, args =
if !shrink_abstract then shrink_entry sign const
- else (const, List.rev (instance_from_named_context sign))
+ else (const, List.rev (Context.Named.to_instance sign))
in
let cd = Entries.DefinitionEntry const in
let decl = (cd, IsProof Lemma) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 098212048..2ae72f4a5 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -9,7 +9,6 @@
open Loc
open Names
open Term
-open Context
open Environ
open Proof_type
open Evd
@@ -33,9 +32,9 @@ val is_quantified_hypothesis : Id.t -> goal sigma -> bool
val introduction : ?check:bool -> Id.t -> unit Proofview.tactic
val refine : constr -> tactic
val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
-val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic
+val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic
val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
-val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
+val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic
val thin : Id.t list -> tactic
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
@@ -50,7 +49,7 @@ val convert_leq : constr -> constr -> unit Proofview.tactic
val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t
val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t
-val find_intro_names : rel_context -> goal sigma -> Id.t list
+val find_intro_names : Context.Rel.t -> goal sigma -> Id.t list
val intro : unit Proofview.tactic
val introf : unit Proofview.tactic
@@ -180,7 +179,7 @@ val revert : Id.t list -> unit Proofview.tactic
(** {6 Resolution tactics. } *)
val apply_type : constr -> constr list -> unit Proofview.tactic
-val bring_hyps : named_context -> unit Proofview.tactic
+val bring_hyps : Context.Named.t -> unit Proofview.tactic
val apply : constr -> unit Proofview.tactic
val eapply : constr -> unit Proofview.tactic
@@ -239,20 +238,20 @@ type elim_scheme = {
elimc: constr with_bindings option;
elimt: types;
indref: global_reference option;
- params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
- nparams: int; (** number of parameters *)
- predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
- npredicates: int; (** Number of predicates *)
- branches: rel_context; (** branchr,...,branch1 *)
- nbranches: int; (** Number of branches *)
- args: rel_context; (** (xni, Ti_ni) ... (x1, Ti_1) *)
- nargs: int; (** number of arguments *)
- indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni)
- if HI is in premisses, None otherwise *)
- concl: types; (** Qi x1...xni HI (f...), HI and (f...)
- are optional and mutually exclusive *)
- indarg_in_concl: bool; (** true if HI appears at the end of conclusion *)
- farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *)
+ params: Context.Rel.t; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+ nparams: int; (** number of parameters *)
+ predicates: Context.Rel.t; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+ npredicates: int; (** Number of predicates *)
+ branches: Context.Rel.t; (** branchr,...,branch1 *)
+ nbranches: int; (** Number of branches *)
+ args: Context.Rel.t; (** (xni, Ti_ni) ... (x1, Ti_1) *)
+ nargs: int; (** number of arguments *)
+ indarg: Context.Rel.Declaration.t option; (** Some (H,I prm1..prmp x1...xni)
+ if HI is in premisses, None otherwise *)
+ concl: types; (** Qi x1...xni HI (f...), HI and (f...)
+ are optional and mutually exclusive *)
+ indarg_in_concl: bool; (** true if HI appears at the end of conclusion *)
+ farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *)
}
val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index a71588fe0..470485438 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -141,7 +141,7 @@ let label_of = function
| ConstructRef ((kn,_),_) -> pi3 (repr_mind kn)
| VarRef id -> Label.of_id id
-let push (r : Context.rel_declaration) (ctx : Context.rel_context) = r :: ctx
+let push (r : Context.Rel.Declaration.t) (ctx : Context.Rel.t) = r :: ctx
let rec traverse current ctx accu t = match kind_of_term t with
| Var id ->
diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli
index f89b39543..21039f571 100644
--- a/toplevel/assumptions.mli
+++ b/toplevel/assumptions.mli
@@ -21,7 +21,7 @@ open Printer
val traverse :
Label.t -> constr ->
(Refset_env.t * Refset_env.t Refmap_env.t *
- (label * Context.rel_context * types) list Refmap_env.t)
+ (label * Context.Rel.t * types) list Refmap_env.t)
(** Collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type). The above warning of
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 98686fb1b..56106928e 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -15,7 +15,6 @@ open Util
open Pp
open Term
open Vars
-open Context
open Termops
open Declarations
open Names
@@ -103,7 +102,7 @@ let mkFullInd (ind,u) n =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
if nparrec > 0
then mkApp (mkIndU (ind,u),
- Array.of_list(extended_rel_list (nparrec+n) lnamesparrec))
+ Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec))
else mkIndU (ind,u)
let check_bool_is_defined () =
@@ -138,7 +137,7 @@ let build_beq_scheme mode kn =
| Name s -> Id.of_string ("eq_"^(Id.to_string s))
| Anonymous -> Id.of_string "eq_A"
in
- let ext_rel_list = extended_rel_list 0 lnamesparrec in
+ let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in
let lift_cnt = ref 0 in
let eqs_typ = List.map (fun aa ->
let a = lift !lift_cnt aa in
@@ -234,7 +233,7 @@ let build_beq_scheme mode kn =
Cn => match Y with ... end |] part *)
let ci = make_case_info env (fst ind) MatchStyle in
let constrs n = get_constructors env (make_ind_family (ind,
- extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in
+ Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
let ar = Array.make n (Lazy.force ff) in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 22baa5e61..28a39b570 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -12,7 +12,6 @@ open Pp
open Names
open Term
open Vars
-open Context
open Termops
open Entries
open Environ
@@ -198,13 +197,13 @@ let build_id_coercion idf_opt source poly =
let val_f =
it_mkLambda_or_LetIn
(mkLambda (Name Namegen.default_dependent_ident,
- applistc vs (extended_rel_list 0 lams),
+ applistc vs (Context.Rel.to_extended_list 0 lams),
mkRel 1))
lams
in
let typ_f =
it_mkProd_wo_LetIn
- (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t))
+ (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t))
lams
in
(* juste pour verification *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9cdb46064..ab18350c5 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -351,7 +351,7 @@ let context poly l =
let evars = ref (Evd.from_env env) in
let _, ((env', fullctx), impls) = interp_context_evars env evars l in
let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
- let fullctx = Context.map_rel_context subst fullctx in
+ let fullctx = Context.Rel.map subst fullctx in
let ce t = Evarutil.check_evars env Evd.empty !evars t in
let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
let ctx =
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 2b7e9e4fe..80ed24629 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Context
open Environ
open Constrexpr
open Typeclasses
@@ -15,9 +14,9 @@ open Libnames
(** Errors *)
-val mismatched_params : env -> constr_expr list -> rel_context -> 'a
+val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a
-val mismatched_props : env -> constr_expr list -> rel_context -> 'a
+val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
(** Instance declaration *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 91cfddb54..500769aca 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -12,7 +12,6 @@ open Util
open Flags
open Term
open Vars
-open Context
open Termops
open Entries
open Environ
@@ -87,7 +86,7 @@ let interp_definition pl bl p red_option c ctypopt =
match ctypopt with
None ->
let subst = evd_comb0 Evd.nf_univ_variables evdref in
- let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+ let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
@@ -100,7 +99,7 @@ let interp_definition pl bl p red_option c ctypopt =
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
let subst = evd_comb0 Evd.nf_univ_variables evdref in
- let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+ let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
@@ -125,7 +124,7 @@ let interp_definition pl bl p red_option c ctypopt =
definition_entry ~types:typ ~poly:p
~univs:uctx body
in
- red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, pl, imps
+ red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
let check_definition (ce, evd, _, imps) =
check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
@@ -566,7 +565,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
(* Compute interpretation metadatas *)
let indimpls = List.map (fun (_, _, impls) -> userimpls @
- lift_implicits (rel_context_nhyps ctx_params) impls) arities in
+ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
@@ -592,11 +591,11 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
let nf x = nf' (nf x) in
let arities = List.map nf' arities in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
- let ctx_params = map_rel_context nf ctx_params in
+ let ctx_params = Context.Rel.map nf ctx_params in
let evd = !evdref in
let pl, uctx = Evd.universe_context ?names:pl evd in
List.iter (check_evars env_params Evd.empty evd) arities;
- iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
+ Context.Rel.iter (check_evars env0 Evd.empty evd) ctx_params;
List.iter (fun (_,ctyps,_) ->
List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
constructors;
@@ -610,7 +609,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
mind_entry_lc = ctypes
}) indl arities aritypoly constructors in
let impls =
- let len = rel_context_nhyps ctx_params in
+ let len = Context.Rel.nhyps ctx_params in
List.map2 (fun indimpls (_,_,cimpls) ->
indimpls, List.map (fun impls ->
userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b6da21e5a..9416b7e7a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -9,7 +9,6 @@
open Names
open Errors
open Util
-open Context
open Term
open Vars
open Entries
@@ -37,8 +36,8 @@ let detype_param = function
let abstract_inductive hyps nparams inds =
let ntyp = List.length inds in
- let nhyp = named_context_length hyps in
- let args = instance_from_named_context (List.rev hyps) in
+ let nhyp = Context.Named.length hyps in
+ let args = Context.Named.to_instance (List.rev hyps) in
let args = Array.of_list args in
let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
let inds' =
@@ -100,7 +99,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
Array.to_list mip.mind_consnames,
Array.to_list lc))
mib.mind_packets in
- let sechyps' = map_named_context (expmod_constr modlist) sechyps in
+ let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in
let (params',inds') = abstract_inductive sechyps' nparams inds in
let abs_ctx = Univ.instantiate_univ_context abs_ctx in
let univs = Univ.UContext.union abs_ctx univs in
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 386e4e3ef..2984a0be8 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -6,10 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Context
open Declarations
open Entries
open Opaqueproof
val process_inductive :
- named_context Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+ Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index a3b973e4d..fd91cfb5c 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -13,7 +13,6 @@ open Declare
*)
open Term
-open Context
open Vars
open Names
open Evd
@@ -44,7 +43,7 @@ let check_evars env evm =
type oblinfo =
{ ev_name: int * Id.t;
- ev_hyps: named_context;
+ ev_hyps: Context.Named.t;
ev_status: Evar_kinds.obligation_definition_status;
ev_chop: int option;
ev_src: Evar_kinds.t Loc.located;
@@ -191,7 +190,7 @@ open Environ
let eterm_obligations env name evm fs ?status t ty =
(* 'Serialize' the evars *)
let nc = Environ.named_context env in
- let nc_len = Context.named_context_length nc in
+ let nc_len = Context.Named.length nc in
let evm = Evarutil.nf_evar_map_undefined evm in
let evl = Evarutil.non_instantiated evm in
let evl = Evar.Map.bindings evl in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c432274a0..408d3fa5f 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -13,7 +13,6 @@ open Names
open Globnames
open Nameops
open Term
-open Context
open Vars
open Environ
open Declarations
@@ -148,8 +147,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
else arity, evars
in
let evars, nf = Evarutil.nf_evars_and_universes evars in
- let newps = map_rel_context nf newps in
- let newfs = map_rel_context nf newfs in
+ let newps = Context.Rel.map nf newps in
+ let newfs = Context.Rel.map nf newfs in
let ce t = Evarutil.check_evars env0 Evd.empty evars t in
List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
@@ -244,8 +243,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
let ctx = Univ.instantiate_univ_context mib.mind_universes in
let indu = indsp, u in
let r = mkIndU (indsp,u) in
- let rp = applist (r, Context.extended_rel_list 0 paramdecls) in
- let paramargs = Context.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
+ let rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in
+ let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*)
let x = Name binder_name in
let fields = instantiate_possibly_recursive_type indu paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
@@ -353,7 +352,7 @@ open Typeclasses
let declare_structure finite poly ctx id idbuild paramimpls params arity template
fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
- let args = Context.extended_rel_list nfields params in
+ let args = Context.Rel.to_extended_list nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
let binder_name =
diff --git a/toplevel/record.mli b/toplevel/record.mli
index eccb5d29d..f68adcec8 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Vernacexpr
open Constrexpr
open Impargs
@@ -22,15 +21,15 @@ val primitive_flag : bool ref
val declare_projections :
inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
- coercion_flag list -> manual_explicitation list list -> rel_context ->
+ coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
(Name.t * bool) list * constant option list
val declare_structure : Decl_kinds.recursivity_kind ->
bool (** polymorphic?*) -> Univ.universe_context ->
Id.t -> Id.t ->
- manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
+ manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
bool (** template arity ? *) ->
- Impargs.manual_explicitation list list -> rel_context -> (** fields *)
+ Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *)
?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
bool -> (** coercion? *)
bool list -> (** field coercions *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7144db494..55e57ec69 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1580,7 +1580,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
(str "No such goal: " ++ int n ++ str "."))
| _ , _ -> raise NoHyp in
let hyps = pf_hyps gl in
- let (id,bdyopt,typ) = Context.lookup_named id hyps in
+ let (id,bdyopt,typ) = Context.Named.lookup id hyps in
let natureofid = match bdyopt with
| None -> "Hypothesis"
| Some bdy ->"Constant (let in)" in