diff options
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 926e2601c..ce9ea7390 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -19,10 +19,9 @@ val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr val get_sort_of : env -> 'a evar_map -> constr -> sorts (*i The following should be merged with mind_specif and put elsewhere - Note : it needs Reduction -i*) + Note : it needs Reduction i*) -(* A light version of mind_specif *) +(* A light version of [mind_specif] *) (* Invariant: We have\\ -- Hnf (fullmind) = DOPN(AppL,[|coremind;..params..;..realargs..|])\\ @@ -30,14 +29,14 @@ i*) *) type mutind_id = inductive_path * constr array -type mutind = - {fullmind : constr; - mind : mutind_id; - nparams : int; - nconstr : int; - params : constr list; - realargs : constr list; - arity : constr};; +type mutind = { + fullmind : constr; + mind : mutind_id; + nparams : int; + nconstr : int; + params : constr list; + realargs : constr list; + arity : constr } (* [try_mutind_of sigma t] raise Induc if [t] is not an inductive type *) val try_mutind_of : env -> 'a Evd.evar_map -> constr -> mutind |