diff options
Diffstat (limited to 'checker/closure.mli')
| -rw-r--r-- | checker/closure.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/checker/closure.mli b/checker/closure.mli index fa302de6..fc147979 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 *) type transparent_state = Idpred.t * Cpred.t @@ -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 @@ -177,6 +177,7 @@ val unfold_reference : clos_infos -> table_key -> fconstr option (* [mind_equiv] checks whether two inductive types are intentionally equal *) val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool +val eq_table_key : table_key -> table_key -> bool (************************************************************************) (*i This is for lazy debug *) |