From d4a2d6a80b57485467d6141f1140c2aee577495f Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 26 May 2011 10:54:02 +0000 Subject: Fixing discriminate for identity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14157 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/elimschemes.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'tactics/elimschemes.mli') diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index a3a8d5edc..06d44550c 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -14,6 +14,7 @@ val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val rec_scheme_kind_from_prop : individual scheme_kind val rect_dep_scheme_kind_from_type : individual scheme_kind +val ind_scheme_kind_from_type : individual scheme_kind val ind_dep_scheme_kind_from_type : individual scheme_kind val rec_dep_scheme_kind_from_type : individual scheme_kind -- cgit v1.2.3