From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 interp/constrextern.mli | 58 +++++++++++++++++++++++++++++++------------------
 1 file changed, 37 insertions(+), 21 deletions(-)

(limited to 'interp/constrextern.mli')

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index f617faa3..8ab70283 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -1,14 +1,16 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
-open Term
 open Termops
+open EConstr
 open Environ
 open Libnames
 open Globnames
@@ -18,13 +20,14 @@ open Constrexpr
 open Notation_term
 open Notation
 open Misctypes
+open Ltac_pretype
 
 (** Translation of pattern, cases pattern, glob_constr and term into syntax
    trees for printing *)
 
-val extern_cases_pattern : Id.Set.t -> cases_pattern -> cases_pattern_expr
-val extern_glob_constr : Id.Set.t -> glob_constr -> constr_expr
-val extern_glob_type : Id.Set.t -> glob_constr -> constr_expr
+val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr
+val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr
+val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr
 val extern_constr_pattern : names_context -> Evd.evar_map ->
   constr_pattern -> constr_expr
 val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr
@@ -37,11 +40,11 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
 
 val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
-val extern_sort : Evd.evar_map -> sorts -> glob_sort
+val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
-  Context.Rel.t -> local_binder list
+  rel_context -> local_binder_expr list
 
 (** Printing options *)
 val print_implicits : bool ref
@@ -55,19 +58,22 @@ val print_projections : bool ref
 
 (** Customization of the global_reference printer *)
 val set_extern_reference :
-  (Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+  (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
 val get_extern_reference :
-  unit -> (Loc.t -> Id.Set.t -> global_reference -> reference)
+  unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
 
-(** This governs printing of implicit arguments. If [with_implicits] is
-   on and not [with_arguments] then implicit args are printed prefixed
-   by "!"; if [with_implicits] and [with_arguments] are both on the
-   function and not the arguments is prefixed by "!" *)
-val with_implicits : ('a -> 'b) -> 'a -> 'b
-val with_arguments : ('a -> 'b) -> 'a -> 'b
+(** WARNING: The following functions are evil due to
+    side-effects. Think of the following case as used in the printer:
 
-(** This forces printing of coercions *)
-val with_coercions : ('a -> 'b) -> 'a -> 'b
+    without_specific_symbols [SynDefRule kn] (pr_glob_constr_env env) c
+
+    vs
+
+    without_specific_symbols [SynDefRule kn] pr_glob_constr_env env c
+
+    which one is wrong? We should turn this kind of state into an
+    explicit argument.
+*)
 
 (** This forces printing universe names of Type\{.\} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b
@@ -80,3 +86,13 @@ val without_specific_symbols : interp_rule list -> ('a -> 'b) -> 'a -> 'b
 
 (** This prints metas as anonymous holes *)
 val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
+
+(** Fine-grained activation and deactivation of notation printing.
+ *)
+val toggle_scope_printing :
+  scope:Notation_term.scope_name -> activate:bool -> unit
+
+val toggle_notation_printing :
+  ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit
+
+
-- 
cgit v1.2.3