aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
blob: 6cc3615f065a04779741de68179bf17f65171358 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Loc
open Pp
open Names
open Libnames
open Glob_term
open Term
open Mod_subst
open Misctypes
open Decl_kinds
open Constrexpr
open Notation_term

(** Topconstr *)

val oldfashion_patterns : bool ref

(** Utilities on constr_expr                                           *)

val replace_vars_constr_expr :
  (Id.t * Id.t) list -> constr_expr -> constr_expr

val free_vars_of_constr_expr : constr_expr -> Id.Set.t
val occur_var_constr_expr : Id.t -> constr_expr -> bool

(** Specific function for interning "in indtype" syntax of "match" *)
val ids_of_cases_indtype : cases_pattern_expr -> Id.t list

val split_at_annot : local_binder list -> Id.t located option -> local_binder list * local_binder list

(** Used in typeclasses *)

val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) ->
   ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b

(** Used in correctness and interface; absence of var capture not guaranteed 
   in pattern-matching clauses and in binders of the form [x,y:T(x)] *)

val map_constr_expr_with_binders :
  (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
      'a -> constr_expr -> constr_expr

val ntn_loc :
  Loc.t -> constr_notation_substitution -> string -> (int * int) list
val patntn_loc :
  Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list

(** For cases pattern parsing errors *)

val error_invalid_pattern_notation : Loc.t -> 'a