diff options
| author | Pierre-Marie Pédrot | 2018-11-19 08:12:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:29:55 +0100 |
| commit | 733cb74a2038ff92156b7209713fc2ea741ccca6 (patch) | |
| tree | ee664936850ce6160d9e3fc3219b9dba7b7ea096 /pretyping/evarconv.mli | |
| parent | ad5aea737ecc639c31dda84322b3550a4d380b47 (diff) | |
Rename TranspState into TransparentState.
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 721a6fad8e..4585fac252 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -21,20 +21,20 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error (** {6 Main unification algorithm for type inference. } *) (** returns exception NotUnifiable with best known evar_map if not unifiable *) -val the_conv_x : env -> ?ts:TranspState.t -> constr -> constr -> evar_map -> evar_map -val the_conv_x_leq : env -> ?ts:TranspState.t -> constr -> constr -> evar_map -> evar_map +val the_conv_x : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map +val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map (** The same function resolving evars by side-effect and catching the exception *) -val conv : env -> ?ts:TranspState.t -> evar_map -> constr -> constr -> evar_map option -val cumul : env -> ?ts:TranspState.t -> evar_map -> constr -> constr -> evar_map option +val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option +val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option (** {6 Unification heuristics. } *) (** Try heuristics to solve pending unification problems and to solve evars with candidates *) -val solve_unif_constraints_with_heuristics : env -> ?ts:TranspState.t -> evar_map -> evar_map +val solve_unif_constraints_with_heuristics : env -> ?ts:TransparentState.t -> evar_map -> evar_map (** Check all pending unification problems are solved and raise an error otherwise *) @@ -54,14 +54,14 @@ val check_conv_record : env -> evar_map -> (** Try to solve problems of the form ?x[args] = c by second-order matching, using typing to select occurrences *) -val second_order_matching : TranspState.t -> env -> evar_map -> +val second_order_matching : TransparentState.t -> env -> evar_map -> EConstr.existential -> occurrences option list -> constr -> evar_map * bool (** Declare function to enforce evars resolution by using typing constraints *) val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit -type unify_fun = TranspState.t -> +type unify_fun = TransparentState.t -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result (** Override default [evar_conv_x] algorithm. *) @@ -72,7 +72,7 @@ val evar_conv_x : unify_fun (**/**) (* For debugging *) -val evar_eqappr_x : ?rhs_is_already_stuck:bool -> TranspState.t * bool -> +val evar_eqappr_x : ?rhs_is_already_stuck:bool -> TransparentState.t * bool -> env -> evar_map -> conv_pb -> state * Cst_stack.t -> state * Cst_stack.t -> Evarsolve.unification_result |