diff options
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 2231e5bc..9270d6e3 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,13 +1,15 @@ (************************************************************************) -(* 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 EConstr open Environ open Reductionops open Evd @@ -36,7 +38,7 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr - val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map -(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *) +[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"] (** Check all pending unification problems are solved and raise an error otherwise *) @@ -46,18 +48,18 @@ val check_problems_are_solved : env -> evar_map -> unit (** Check if a canonical structure is applicable *) val check_conv_record : env -> evar_map -> - constr * types Stack.t -> constr * types Stack.t -> - Univ.universe_context_set * (constr * constr) + state -> state -> + Univ.ContextSet.t * (constr * constr) * constr * constr list * (constr Stack.t * constr Stack.t) * - (constr Stack.t * types Stack.t) * - (constr Stack.t * types Stack.t) * constr * + (constr Stack.t * constr Stack.t) * + (constr Stack.t * constr Stack.t) * constr * (int option * constr) (** Try to solve problems of the form ?x[args] = c by second-order matching, using typing to select occurrences *) val second_order_matching : transparent_state -> env -> evar_map -> - existential -> occurrences option list -> constr -> evar_map * bool + EConstr.existential -> occurrences option list -> constr -> evar_map * bool (** Declare function to enforce evars resolution by using typing constraints *) @@ -80,3 +82,5 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool -> Evarsolve.unification_result (**/**) +(** {6 Functions to deal with impossible cases } *) +val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set |