diff options
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index a80f7a62..5cb6fc97 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: closure.mli 11897 2009-02-09 19:28:02Z barras $ i*) +(*i $Id$ i*) (*i*) open Pp @@ -24,7 +24,7 @@ val with_stats: 'a Lazy.t -> 'a (*s Delta implies all consts (both global (= by [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's. - Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of + Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) @@ -102,7 +102,7 @@ type fconstr type fterm = | FRel of int | FAtom of constr (* Metas and Sorts *) - | FCast of fconstr * cast_kind * fconstr + | FCast of fconstr * cast_kind * fconstr | FFlex of table_key | FInd of inductive | FConstruct of constructor @@ -179,9 +179,7 @@ val whd_stack : (* [unfold_reference] unfolds references in a [fconstr] *) val unfold_reference : clos_infos -> table_key -> fconstr option -(* [mind_equiv] checks whether two inductive types are intentionally equal *) -val mind_equiv : env -> inductive -> inductive -> bool -val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool +val eq_table_key : table_key -> table_key -> bool (************************************************************************) (*i This is for lazy debug *) |