diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cbv.ml | 2 | ||||
| -rw-r--r-- | pretyping/cbv.mli | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 2 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 2 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 8 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 4 | ||||
| -rw-r--r-- | pretyping/retyping.mli | 2 | ||||
| -rw-r--r-- | pretyping/typing.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
10 files changed, 15 insertions, 15 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index a2155697e..cb0fc3257 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -71,7 +71,7 @@ and cbv_stack = | TOP | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - | PROJ of projection * Declarations.projection_body * cbv_stack + | PROJ of Projection.t * Declarations.projection_body * cbv_stack (* les vars pourraient etre des constr, cela permet de retarder les lift: utile ?? *) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 2ac59911c..cdaa39c53 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -41,7 +41,7 @@ and cbv_stack = | TOP | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - | PROJ of projection * Declarations.projection_body * cbv_stack + | PROJ of Projection.t * Declarations.projection_body * cbv_stack val shift_value : int -> cbv_value -> cbv_value diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 627430708..9270d6e3a 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -38,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 *) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 9b21599b6..3f05c58c4 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -63,7 +63,7 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result -(** @deprecated Alias for [reconsider_unif_constraints] *) +[@@ocaml.deprecated "Alias for [reconsider_unif_constraints]"] val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> alias list option diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 296f25d3f..b0d714b03 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -129,8 +129,8 @@ val allowed_sorts : env -> inductive -> Sorts.family list val has_dependent_elim : mutual_inductive_body -> bool (** Primitive projections *) -val projection_nparams : projection -> int -val projection_nparams_env : env -> projection -> int +val projection_nparams : Projection.t -> int +val projection_nparams_env : env -> Projection.t -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> EConstr.t -> EConstr.types -> types diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 9e3e68f05..360c6e86e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -275,12 +275,12 @@ sig type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list @@ -332,12 +332,12 @@ struct type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 29dc3ed0f..b8ac085a7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -70,12 +70,12 @@ module Stack : sig type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 40424ead4..2aff0c777 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -50,6 +50,6 @@ val type_of_global_reference_knowing_conclusion : val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list -val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr +val expand_projection : env -> evar_map -> Names.Projection.t -> constr -> constr list -> constr val print_retype_error : retype_error -> Pp.t diff --git a/pretyping/typing.mli b/pretyping/typing.mli index fe83a2cc8..4905adf1f 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -55,4 +55,4 @@ val judge_of_abstraction : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment -val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment +val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f2f922fd5..ca03b96ab 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -466,7 +466,7 @@ let use_metas_pattern_unification sigma flags nb l = type key = | IsKey of CClosure.table_key - | IsProj of projection * EConstr.constr + | IsProj of Projection.t * EConstr.constr let expand_table_key env = function | ConstKey cst -> constant_opt_value_in env cst |