From accde4d40c89f0a40caacb9e91db61f204b05918 Mon Sep 17 00:00:00 2001
From: Thomas Sibut-Pinote
Date: Tue, 23 Jun 2015 19:10:25 +0200
Subject: Added support for a side effect on constants in reduction functions.

This exports two functions:

- declare_reduction_effect: to declare a hook to be applied when some
  constant are visited during the execution of some reduction functions
  (primarily cbv, but also cbn, simpl, hnf, ...).
- set_reduction_effect: to declare a constant on which a given effect
  hook should be called.

Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin.

Added support for printing effect in functions of tacred.ml.
---
 kernel/cClosure.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 077756ac74..69a5e79b45 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -187,7 +187,7 @@ val create_clos_infos :
   ?evars:(existential->constr option) -> reds -> env -> clos_infos
 val oracle_of_infos : clos_infos -> Conv_oracle.oracle
 
-val env_of_infos : clos_infos -> env
+val env_of_infos : 'a infos -> env
 
 val infos_with_reds : clos_infos -> reds -> clos_infos
 
-- 
cgit v1.2.3


From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 kernel/retroknowledge.ml | 2 +-
 kernel/term.ml           | 3 ++-
 kernel/term.mli          | 5 ++++-
 3 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 970bc0fcc5..ea53d00d7b 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -83,7 +83,7 @@ type flags = {fastcomputation : bool}
 (* The [proactive] knowledge contains the mapping [field->entry]. *)
 
 module Proactive =
-  Map.Make (struct type t = field let compare = compare end)
+  Map.Make (struct type t = field let compare = Pervasives.compare end)
 
 type proactive = entry Proactive.t
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 07a85329ef..b90718358e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -143,7 +143,8 @@ let leq_constr_univs = Constr.leq_constr_univs
 let eq_constr_nounivs = Constr.eq_constr_nounivs
 
 let kind_of_term = Constr.kind
-let constr_ord = Constr.compare
+let compare = Constr.compare
+let constr_ord = compare
 let fold_constr = Constr.fold
 let map_puniverses = Constr.map_puniverses
 let map_constr = Constr.map
diff --git a/kernel/term.mli b/kernel/term.mli
index 241ef322fa..e729439f01 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -447,9 +447,12 @@ val eq_constr_nounivs : constr -> constr -> bool
 val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
 (** Alias for [Constr.kind] *)
 
-val constr_ord : constr -> constr -> int
+val compare : constr -> constr -> int
 (** Alias for [Constr.compare] *)
 
+val constr_ord : constr -> constr -> int
+(** Alias for [Term.compare] *)
+
 val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 (** Alias for [Constr.fold] *)
 
-- 
cgit v1.2.3