diff options
| author | filliatr | 1999-08-30 13:17:26 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-30 13:17:26 +0000 |
| commit | f1874a538ef7e5886b72c2ec2ce21b23d05aa8d7 (patch) | |
| tree | d54f85de98bbc0a137a3edeed213918a46e26374 /kernel/instantiate.ml | |
| parent | 19d21ec59b69a7bd5a8e4e77794e85fed6b48d39 (diff) | |
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
Diffstat (limited to 'kernel/instantiate.ml')
| -rw-r--r-- | kernel/instantiate.ml | 6 |
1 files changed, 6 insertions, 0 deletions
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) + |