From 96876c750e05108e07dc1f29fa8db53f35f62f95 Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 22 May 2008 16:07:45 +0000
Subject: fixed dependency problems with the checker

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10970 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/term.mli | 111 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 111 insertions(+)
 create mode 100644 checker/term.mli

(limited to 'checker/term.mli')

diff --git a/checker/term.mli b/checker/term.mli
new file mode 100644
index 000000000..30a2c03a5
--- /dev/null
+++ b/checker/term.mli
@@ -0,0 +1,111 @@
+open Names
+
+type existential_key = int
+type metavariable = int
+type case_style =
+    LetStyle
+  | IfStyle
+  | LetPatternStyle
+  | MatchStyle
+  | RegularStyle
+type case_printing = { ind_nargs : int; style : case_style; }
+type case_info = {
+  ci_ind : inductive;
+  ci_npar : int;
+  ci_cstr_nargs : int array;
+  ci_pp_info : case_printing;
+}
+type contents = Pos | Null
+type sorts = Prop of contents | Type of Univ.universe
+type sorts_family = InProp | InSet | InType
+val family_of_sort : sorts -> sorts_family
+type 'a pexistential = existential_key * 'a array
+type 'a prec_declaration = name array * 'a array * 'a array
+type 'a pfixpoint = (int array * int) * 'a prec_declaration
+type 'a pcofixpoint = int * 'a prec_declaration
+type cast_kind = VMcast | DEFAULTcast
+type constr =
+    Rel of int
+  | Var of identifier
+  | Meta of metavariable
+  | Evar of constr pexistential
+  | Sort of sorts
+  | Cast of constr * cast_kind * constr
+  | Prod of name * constr * constr
+  | Lambda of name * constr * constr
+  | LetIn of name * constr * constr * constr
+  | App of constr * constr array
+  | Const of constant
+  | Ind of inductive
+  | Construct of constructor
+  | Case of case_info * constr * constr * constr array
+  | Fix of constr pfixpoint
+  | CoFix of constr pcofixpoint
+type existential = constr pexistential
+type rec_declaration = constr prec_declaration
+type fixpoint = constr pfixpoint
+type cofixpoint = constr pcofixpoint
+val strip_outer_cast : constr -> constr
+val collapse_appl : constr -> constr
+val decompose_app : constr -> constr * constr list
+val applist : constr * constr list -> constr
+val iter_constr_with_binders :
+  ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
+exception LocalOccur
+val closedn : int -> constr -> bool
+val closed0 : constr -> bool
+val noccurn : int -> constr -> bool
+val noccur_between : int -> int -> constr -> bool
+val noccur_with_meta : int -> int -> constr -> bool
+val map_constr_with_binders :
+  ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+val exliftn : Esubst.lift -> constr -> constr
+val liftn : int -> int -> constr -> constr
+val lift : int -> constr -> constr
+type info = Closed | Open | Unknown
+type 'a substituend = { mutable sinfo : info; sit : 'a; }
+val lift_substituend : int -> constr substituend -> constr
+val make_substituend : 'a -> 'a substituend
+val substn_many : constr substituend array -> int -> constr -> constr
+val substnl : constr list -> int -> constr -> constr
+val substl : constr list -> constr -> constr
+val subst1 : constr -> constr -> constr
+
+type named_declaration = identifier * constr option * constr
+type rel_declaration = name * constr option * constr
+val map_named_declaration :
+  (constr -> constr) -> named_declaration -> named_declaration
+val map_rel_declaration :
+  (constr -> constr) -> rel_declaration -> rel_declaration
+val fold_named_declaration :
+  (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a
+val fold_rel_declaration :
+  (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
+type named_context = named_declaration list
+val empty_named_context : named_context
+val fold_named_context :
+  (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
+type section_context = named_context
+type rel_context = rel_declaration list
+val empty_rel_context : rel_context
+val rel_context_length : rel_context -> int
+val rel_context_nhyps : rel_context -> int
+val fold_rel_context :
+  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val map_context : (constr -> constr) -> named_context -> named_context
+val map_rel_context : (constr -> constr) -> rel_context -> rel_context
+val extended_rel_list : int -> rel_context -> constr list
+val compose_lam : (name * constr) list -> constr -> constr
+val decompose_lam : constr -> (name * constr) list * constr
+val decompose_lam_n_assum : int -> constr -> rel_context * constr
+val mkProd_or_LetIn : name * constr option * constr -> constr -> constr
+val it_mkProd_or_LetIn : constr -> rel_context -> constr
+val decompose_prod_assum : constr -> rel_context * constr
+val decompose_prod_n_assum : int -> constr -> rel_context * constr
+
+type arity = rel_context * sorts
+val mkArity : arity -> constr
+val destArity : constr -> arity
+val isArity : constr -> bool
+val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+val eq_constr : constr -> constr -> bool
-- 
cgit v1.2.3