From 5fa47f1258408541150e2e4c26d60ff694e7c1bc Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:37 +0000 Subject: locus.mli for occurrences+clauses, misctypes.mli for various little things Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/lib.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 40a427e49..ff7e9b841 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -395,14 +395,14 @@ let find_opening_node id = - the list of variables on which each inductive depends in this section - the list of substitution to do at section closing *) -type binding_kind = Explicit | Implicit -type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types +type variable_info = Names.identifier * Decl_kinds.binding_kind * Term.constr option * Term.types type variable_context = variable_info list type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t let sectab = - ref ([] : ((Names.identifier * binding_kind) list * Cooking.work_list * abstr_list) list) + ref ([] : ((Names.identifier * Decl_kinds.binding_kind) list * + Cooking.work_list * abstr_list) list) let add_section () = sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab -- cgit v1.2.3