diff options
| author | herbelin | 2006-05-19 09:29:54 +0000 |
|---|---|---|
| committer | herbelin | 2006-05-19 09:29:54 +0000 |
| commit | a13575eeaf69ec3dadb9b3c6a3e365a7d8371390 (patch) | |
| tree | 888718c8fd5b200aae90be89fbd16339ac40f13d /interp | |
| 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 'interp')
| -rw-r--r-- | interp/constrextern.ml | 14 | ||||
| -rw-r--r-- | interp/constrextern.mli | 1 |
2 files changed, 9 insertions, 6 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e3d4d1a4d6..e73e88587b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -623,6 +623,11 @@ let extern_optimal_prim_token scopes r r' = (**********************************************************************) (* mapping rawterms to constr_expr *) +let extern_rawsort = function + | RProp _ as s -> s + | RType (Some _) as s when !print_universes -> s + | RType _ -> RType None + let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try @@ -740,12 +745,7 @@ let rec extern inctx scopes vars r = in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) - | RSort (loc,s) -> - let s = match s with - | RProp _ -> s - | RType (Some _) when !print_universes -> s - | RType _ -> RType None in - CSort (loc,s) + | RSort (loc,s) -> CSort (loc,extern_rawsort s) | RHole (loc,e) -> CHole loc @@ -873,6 +873,8 @@ let extern_type at_top env t = let r = Detyping.detype at_top avoid (names_of_rel_context env) t in extern_rawtype (vars_of_env env) r +let extern_sort s = extern_rawsort (detype_sort s) + (******************************************************************) (* Main translation function from pattern -> constr_expr *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 37f7369ad6..0ffb8c333a 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -41,6 +41,7 @@ val extern_constr : bool -> env -> constr -> constr_expr val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr val extern_reference : loc -> Idset.t -> global_reference -> reference val extern_type : bool -> env -> types -> constr_expr +val extern_sort : sorts -> rawsort (* Printing options *) val print_implicits : bool ref |