diff options
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index e4a85b84..7fb4f7ba 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: retyping.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: retyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Term @@ -44,7 +44,7 @@ let type_of_var env id = with Not_found -> anomaly ("type_of: variable "^(string_of_id id)^" unbound") -let retype sigma = +let retype ?(polyprop=true) sigma = let rec type_of env cstr= match kind_of_term cstr with | Meta n -> @@ -129,7 +129,7 @@ let retype sigma = match kind_of_term c with | Ind ind -> let (_,mip) = lookup_mind_specif env ind in - Inductive.type_of_inductive_knowing_parameters env mip argtyps + Inductive.type_of_inductive_knowing_parameters ~polyprop env mip argtyps | Const cst -> let t = constant_type env cst in Typeops.type_of_constant_knowing_parameters env t argtyps @@ -140,8 +140,10 @@ let retype sigma = in type_of, sort_of, sort_family_of, type_of_global_reference_knowing_parameters -let get_sort_of env sigma t = let _,f,_,_ = retype sigma in f env t -let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma in f env c +let get_sort_of ?(polyprop=true) env sigma t = + let _,f,_,_ = retype ~polyprop sigma in f env t +let get_sort_family_of ?(polyprop=true) env sigma c = + let _,_,f,_ = retype ~polyprop sigma in f env c let type_of_global_reference_knowing_parameters env sigma c args = let _,_,_,f = retype sigma in f env c args @@ -161,8 +163,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* We are outside the kernel: we take fresh universes *) (* to avoid tactics and co to refresh universes themselves *) -let get_type_of ?(refresh=true) env sigma c = - let f,_,_,_ = retype sigma in +let get_type_of ?(polyprop=true) ?(refresh=true) env sigma c = + let f,_,_,_ = retype ~polyprop sigma in let t = f env c in if refresh then refresh_universes t else t |