From b5657ff1939c6872ee3ccaeaf180a2f3da9e1876 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 14 Jan 2005 14:30:06 +0000
Subject: Inductive.{type_of_inductive,type_of_constructor,arities_of_specif}
 changed to accept a mind_specif (a couple mutual_inductive_body *
 one_inductive_body) instead of looking it up in the environment. A version of
 the same functions with the old type is put in Inductiveops (outside the
 kernel).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/prettyp.ml | 2 +-
 parsing/search.ml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 7df78fe61c..bbbbc31800 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -507,7 +507,7 @@ let print_opaque_name qid =
     | IndRef (sp,_) ->
         print_mutual sp
     | ConstructRef cstr -> 
-	let ty = Inductive.type_of_constructor env cstr in
+	let ty = Inductiveops.type_of_constructor env cstr in
 	print_typed_value (mkConstruct cstr, ty)
     | VarRef id ->
         let (_,c,ty) = lookup_named id env in 
diff --git a/parsing/search.ml b/parsing/search.ml
index de7e497b18..8435f4b4bb 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -34,7 +34,7 @@ open Nametab
 
 let print_constructors indsp fn env nconstr =
   for i = 1 to nconstr do
-    fn (ConstructRef (indsp,i)) env (Inductive.type_of_constructor env (indsp,i))
+    fn (ConstructRef (indsp,i)) env (Inductiveops.type_of_constructor env (indsp,i))
   done
 
 let rec head_const c = match kind_of_term c with
-- 
cgit v1.2.3