diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 7 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 2 |
2 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1f6e4a86b7..ec6edcbdfd 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -348,6 +348,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | _ -> RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl) +let detype_sort = function + | Prop c -> RProp c + | Type u -> RType (Some u) + (**********************************************************************) (* Main detyping function *) @@ -368,8 +372,7 @@ let rec detype isgoal avoid env t = let _ = Global.lookup_named id in RRef (dl, VarRef id) with _ -> RVar (dl, id)) - | Sort (Prop c) -> RSort (dl,RProp c) - | Sort (Type u) -> RSort (dl,RType (Some u)) + | Sort s -> RSort (dl,detype_sort s) | Cast (c1,k,c2) -> RCast(dl,detype isgoal avoid env c1, k, detype isgoal avoid env c2) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 3068f97c28..7f979d6e6d 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -38,6 +38,8 @@ val detype_case : identifier list -> inductive * case_style * int * int array * int -> 'a option -> 'a -> 'a array -> rawconstr +val detype_sort : sorts -> rawsort + (* look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_renamed : env -> constr -> identifier -> int option val lookup_index_as_renamed : env -> constr -> int -> int option |