From f1874a538ef7e5886b72c2ec2ce21b23d05aa8d7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 30 Aug 1999 13:17:26 +0000
Subject: ajout des inductifs (sans types singletons pour l'instant)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@32 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/instantiate.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/instantiate.ml')

diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 6302badc22..9b4c1ae710 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -8,6 +8,7 @@ open Generic
 open Term
 open Sign
 open Constant
+open Inductive
 open Evd
 open Environ
 
@@ -101,3 +102,8 @@ let const_abst_opt_value env c =
     | DOPN(Abst sp,_) ->
 	if evaluable_abst env c then Some (abst_value env c) else None
     | _ -> invalid_arg "const_abst_opt_value"
+
+let mis_lc env mis =
+  instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
+    (Array.to_list mis.mis_args)
+
-- 
cgit v1.2.3