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/constrextern.mli | |
| 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/constrextern.mli')
| -rw-r--r-- | interp/constrextern.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |