diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml (renamed from intf/constrexpr.mli) | 0 | ||||
| -rw-r--r-- | intf/decl_kinds.ml (renamed from intf/decl_kinds.mli) | 0 | ||||
| -rw-r--r-- | intf/evar_kinds.ml (renamed from intf/evar_kinds.mli) | 7 | ||||
| -rw-r--r-- | intf/extend.ml (renamed from intf/extend.mli) | 0 | ||||
| -rw-r--r-- | intf/genredexpr.ml (renamed from intf/genredexpr.mli) | 0 | ||||
| -rw-r--r-- | intf/glob_term.ml (renamed from intf/glob_term.mli) | 2 | ||||
| -rw-r--r-- | intf/intf.mllib | 12 | ||||
| -rw-r--r-- | intf/locus.ml (renamed from intf/locus.mli) | 0 | ||||
| -rw-r--r-- | intf/misctypes.ml (renamed from intf/misctypes.mli) | 0 | ||||
| -rw-r--r-- | intf/notation_term.ml (renamed from intf/notation_term.mli) | 0 | ||||
| -rw-r--r-- | intf/pattern.ml (renamed from intf/pattern.mli) | 0 | ||||
| -rw-r--r-- | intf/tactypes.ml (renamed from intf/tactypes.mli) | 3 | ||||
| -rw-r--r-- | intf/vernacexpr.ml (renamed from intf/vernacexpr.mli) | 0 |
13 files changed, 19 insertions, 5 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.ml index 614c097b5a..614c097b5a 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.ml diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.ml index 8254b1b802..8254b1b802 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.ml diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.ml index 470ad2a23b..ac0d96e96b 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.ml @@ -8,6 +8,7 @@ open Names open Globnames +open Misctypes (** The kinds of existential variable *) @@ -16,17 +17,19 @@ open Globnames type obligation_definition_status = Define of bool | Expand +type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar + type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t | NamedHole of Id.t (* coming from some ?[id] syntax *) - | QuestionMark of obligation_definition_status + | QuestionMark of obligation_definition_status * Name.t | CasesType of bool (* true = a subterm of the type *) | InternalHole | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase - | MatchingVar of bool * Id.t + | MatchingVar of matching_var_kind | VarInstance of Id.t | SubEvar of Constr.existential_key diff --git a/intf/extend.mli b/intf/extend.ml index 99401d06f0..99401d06f0 100644 --- a/intf/extend.mli +++ b/intf/extend.ml diff --git a/intf/genredexpr.mli b/intf/genredexpr.ml index 2a542e0ff2..2a542e0ff2 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.ml diff --git a/intf/glob_term.mli b/intf/glob_term.ml index 33c71884a2..5da20c9d1c 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.ml @@ -39,7 +39,7 @@ type glob_constr_r = (** An identifier that cannot be regarded as "GRef". Bound variables are typically represented this way. *) | GEvar of existential_name * (Id.t * glob_constr) list - | GPatVar of bool * patvar (** Used for patterns only *) + | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *) | GApp of glob_constr * glob_constr list | GLambda of Name.t * binding_kind * glob_constr * glob_constr | GProd of Name.t * binding_kind * glob_constr * glob_constr diff --git a/intf/intf.mllib b/intf/intf.mllib new file mode 100644 index 0000000000..523e4b2650 --- /dev/null +++ b/intf/intf.mllib @@ -0,0 +1,12 @@ +Constrexpr +Evar_kinds +Genredexpr +Locus +Notation_term +Tactypes +Decl_kinds +Extend +Glob_term +Misctypes +Pattern +Vernacexpr diff --git a/intf/locus.mli b/intf/locus.ml index 57b398ab46..57b398ab46 100644 --- a/intf/locus.mli +++ b/intf/locus.ml diff --git a/intf/misctypes.mli b/intf/misctypes.ml index 2ab70a78ef..2ab70a78ef 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.ml diff --git a/intf/notation_term.mli b/intf/notation_term.ml index 753fa657a8..753fa657a8 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.ml diff --git a/intf/pattern.mli b/intf/pattern.ml index 48381cacdc..48381cacdc 100644 --- a/intf/pattern.mli +++ b/intf/pattern.ml diff --git a/intf/tactypes.mli b/intf/tactypes.ml index ef90b911c5..5c1d31946c 100644 --- a/intf/tactypes.mli +++ b/intf/tactypes.ml @@ -22,8 +22,7 @@ open Misctypes type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern -type 'a delayed_open = - { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } +type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a type delayed_open_constr = EConstr.constr delayed_open type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.ml index ab440c6b71..ab440c6b71 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.ml |