diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-19 09:29:54 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-19 09:29:54 +0000 |
| commit | a13575eeaf69ec3dadb9b3c6a3e365a7d8371390 (patch) | |
| tree | 888718c8fd5b200aae90be89fbd16339ac40f13d /pretyping | |
| parent | a171cb800c5cd7f4faf31f3fd20922d092bfd16c (diff) | |
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8831 85f007b7-540e-0410-9357-904b9bb8a0f7
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 1f6e4a86b..ec6edcbdf 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 3068f97c2..7f979d6e6 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 |