diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 3 | ||||
| -rw-r--r-- | interp/declare.mli | 1 | ||||
| -rw-r--r-- | interp/impargs.ml | 9 | ||||
| -rw-r--r-- | interp/impargs.mli | 1 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 5 |
5 files changed, 4 insertions, 15 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 175f9c66df..4371b15c82 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -430,9 +430,6 @@ let assumption_message id = discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") -let register_message id = - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is registered") - (** Monomorphic universes need to survive sections. *) let input_universe_context : Univ.ContextSet.t -> Libobject.obj = diff --git a/interp/declare.mli b/interp/declare.mli index 6f53d6872b..8f1e73c88c 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -74,7 +74,6 @@ val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool val definition_message : Id.t -> unit val assumption_message : Id.t -> unit -val register_message : Id.t -> unit val fixpoint_message : int array option -> Id.t list -> unit val cofixpoint_message : Id.t list -> unit val recursive_message : bool (** true = fixpoint *) -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 7e8f2f4f3d..6fd52d98dd 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -120,12 +120,7 @@ let argument_position_eq p1 p2 = match p1, p2 with | Hyp h1, Hyp h2 -> Int.equal h1 h2 | _ -> false -let explicitation_eq ex1 ex2 = match ex1, ex2 with -| ExplByPos (i1, id1), ExplByPos (i2, id2) -> - Int.equal i1 i2 && Option.equal Id.equal id1 id2 -| ExplByName id1, ExplByName id2 -> - Id.equal id1 id2 -| _ -> false +let explicitation_eq = Constrexpr_ops.explicitation_eq type implicit_explanation = | DepRigid of argument_position @@ -380,7 +375,7 @@ let flatten_explicitations l autoimps = | (Name id,_)::imps -> let value, l' = try - let eq = explicitation_eq in + let eq = Constrexpr_ops.explicitation_eq in let flags = List.assoc_f eq (ExplByName id) l in Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l with Not_found -> assoc_by_pos k l diff --git a/interp/impargs.mli b/interp/impargs.mli index 4afc2af5e9..43c26b024f 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -138,4 +138,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool + [@@ocaml.deprecated "Use Constrexpr_ops.explicitation_eq instead (since 8.10)"] (** Equality on [explicitation]. *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 890c24e633..7d7e10a05b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -908,11 +908,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) (* TODO: look at the consequences for alp *) alp, add_env alp sigma var (DAst.make @@ GVar id) -let force_cases_pattern c = - DAst.make ?loc:c.CAst.loc (DAst.get c) - let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in + let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let patl' = Id.List.assoc var binders in |