diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-26 18:52:24 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-26 18:52:24 +0000 |
commit | 60de53d159c85b8300226a61aa502a7e0dd2f04b (patch) | |
tree | e542ed90d58872a75816d451ae26e38fa7b1d9f9 /kernel/declareops.mli | |
parent | 7dd28b4772251af6ae3641ec63a8251153915e21 (diff) |
kernel/declarations becomes a pure mli
- constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
- the functions that were in declarations.ml (mostly substitution utilities
and hashcons) are now in kernel/declareops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declareops.mli')
-rw-r--r-- | kernel/declareops.mli | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli new file mode 100644 index 000000000..1616e4639 --- /dev/null +++ b/kernel/declareops.mli @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Declarations +open Mod_subst +open Lazyconstr + +(** Operations concerning types in [Declarations] : + [constant_body], [mutual_inductive_body], [module_body] ... *) + +(** {6 Constants} *) + +val subst_const_def : substitution -> constant_def -> constant_def +val subst_const_body : substitution -> constant_body -> constant_body + +(** Is there a actual body in const_body or const_body_opaque ? *) + +val constant_has_body : constant_body -> bool + +(** Accessing const_body_opaque or const_body *) + +val body_of_constant : constant_body -> constr_substituted option + +val is_opaque : constant_body -> bool + + +(** {6 Inductive types} *) + +val eq_recarg : recarg -> recarg -> bool + +val subst_recarg : substitution -> recarg -> recarg + +val mk_norec : wf_paths +val mk_paths : recarg -> wf_paths list array -> wf_paths +val dest_recarg : wf_paths -> recarg +val dest_subterms : wf_paths -> wf_paths list array +val recarg_length : wf_paths -> int -> int + +val subst_wf_paths : substitution -> wf_paths -> wf_paths + +val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body + + +(** {6 Hash-consing} *) + +(** Here, strictly speaking, we don't perform true hash-consing + of the structure, but simply hash-cons all inner constr + and other known elements *) + +val hcons_const_body : constant_body -> constant_body +val hcons_mind : mutual_inductive_body -> mutual_inductive_body |