From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:56:25 +0000 Subject: Modulification of identifier git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/indrec.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/indrec.mli') diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 1bf5fd90c..610a7bf39 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -63,6 +63,6 @@ val weaken_sort_scheme : sorts -> int -> constr -> types -> constr * types val lookup_eliminator : inductive -> sorts_family -> constr val elimination_suffix : sorts_family -> string -val make_elimination_ident : identifier -> sorts_family -> identifier +val make_elimination_ident : Id.t -> sorts_family -> Id.t val case_suffix : string -- cgit v1.2.3