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

---
 intf/constrexpr.mli | 150 ----------------------------------------------------
 1 file changed, 150 deletions(-)
 delete mode 100644 intf/constrexpr.mli

(limited to 'intf/constrexpr.mli')

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
deleted file mode 100644
index 0cbb2957..00000000
--- a/intf/constrexpr.mli
+++ /dev/null
@@ -1,150 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Loc
-open Names
-open Libnames
-open Misctypes
-open Decl_kinds
-
-(** {6 Concrete syntax for terms } *)
-
-(** [constr_expr] is the abstract syntax tree produced by the parser *)
-
-type notation = string
-
-type explicitation =
-  | ExplByPos of int * Id.t option
-  | ExplByName of Id.t
-
-type binder_kind =
-  | Default of binding_kind
-  | Generalized of binding_kind * binding_kind * bool
-      (** Inner binding, outer bindings, typeclass-specific flag
-	 for implicit generalization of superclasses *)
-
-type abstraction_kind = AbsLambda | AbsPi
-
-type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
-
-type prim_token =
-  | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *)
-  | String of string
-
-type raw_cases_pattern_expr =
-  | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
-  | RCPatCstr of Loc.t * Globnames.global_reference
-    * raw_cases_pattern_expr list * raw_cases_pattern_expr list
-  (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *)
-  | RCPatAtom of Loc.t * Id.t option
-  | RCPatOr of Loc.t * raw_cases_pattern_expr list
-
-type instance_expr = Misctypes.glob_level list
-
-type cases_pattern_expr =
-  | CPatAlias of Loc.t * cases_pattern_expr * Id.t
-  | CPatCstr of Loc.t * reference
-    * cases_pattern_expr list option * cases_pattern_expr list
-  (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
-  | CPatAtom of Loc.t * reference option
-  | CPatOr of Loc.t * cases_pattern_expr list
-  | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution
-    * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
-				  (notation n applied with substitution l1)
-				  applied to arguments l2 *)
-  | CPatPrim of Loc.t * prim_token
-  | CPatRecord of Loc.t * (reference * cases_pattern_expr) list
-  | CPatDelimiters of Loc.t * string * cases_pattern_expr
-  | CPatCast of Loc.t * cases_pattern_expr * constr_expr
-
-and cases_pattern_notation_substitution =
-    cases_pattern_expr list *     (** for constr subterms *)
-    cases_pattern_expr list list  (** for recursive notations *)
-
-and constr_expr =
-  | CRef of reference * instance_expr option
-  | CFix of Loc.t * Id.t located * fix_expr list
-  | CCoFix of Loc.t * Id.t located * cofix_expr list
-  | CProdN of Loc.t * binder_expr list * constr_expr
-  | CLambdaN of Loc.t * binder_expr list * constr_expr
-  | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr
-  | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list
-  | CApp of Loc.t * (proj_flag * constr_expr) *
-      (constr_expr * explicitation located option) list
-  | CRecord of Loc.t * (reference * constr_expr) list
-
-  (* representation of the "let" and "match" constructs *)
-  | CCases of Loc.t                 (* position of the "match" keyword *)
-	      * case_style          (* determines whether this value represents "let" or "match" construct *)
-	      * constr_expr option  (* return-clause *)
-	      * case_expr list
-	      * branch_expr list    (* branches *)
-
-  | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) *
-      constr_expr * constr_expr
-  | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option)
-      * constr_expr * constr_expr
-  | CHole of Loc.t * Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
-  | CPatVar of Loc.t * patvar
-  | CEvar of Loc.t * Glob_term.existential_name * (Id.t * constr_expr) list
-  | CSort of Loc.t * glob_sort
-  | CCast of Loc.t * constr_expr * constr_expr cast_type
-  | CNotation of Loc.t * notation * constr_notation_substitution
-  | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr
-  | CPrim of Loc.t * prim_token
-  | CDelimiters of Loc.t * string * constr_expr
-
-and case_expr = constr_expr                 (* expression that is being matched *)
-	      * Name.t located option       (* as-clause *)
-	      * cases_pattern_expr option   (* in-clause *)
-
-and branch_expr =
-  Loc.t * cases_pattern_expr list located list * constr_expr
-
-and binder_expr =
-  Name.t located list * binder_kind * constr_expr
-
-and fix_expr =
-    Id.t located * (Id.t located option * recursion_order_expr) *
-      local_binder list * constr_expr * constr_expr
-
-and cofix_expr =
-    Id.t located * local_binder list * constr_expr * constr_expr
-
-and recursion_order_expr =
-  | CStructRec
-  | CWfRec of constr_expr
-  | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
-
-(** Anonymous defs allowed ?? *)
-and local_binder =
-  | LocalRawDef of Name.t located * constr_expr
-  | LocalRawAssum of Name.t located list * binder_kind * constr_expr
-  | LocalPattern of Loc.t * cases_pattern_expr * constr_expr option
-
-and constr_notation_substitution =
-    constr_expr list *      (** for constr subterms *)
-    constr_expr list list * (** for recursive notations *)
-    local_binder list list (** for binders subexpressions *)
-
-type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr
-
-and typeclass_context = typeclass_constraint list
-
-type constr_pattern_expr = constr_expr
-
-(** Concrete syntax for modules and module types *)
-
-type with_declaration_ast =
-  | CWith_Module of Id.t list located * qualid located
-  | CWith_Definition of Id.t list located * constr_expr
-
-type module_ast =
-  | CMident of qualid located
-  | CMapply of Loc.t * module_ast * module_ast
-  | CMwith of Loc.t * module_ast * with_declaration_ast
-- 
cgit v1.2.3