Add a boolean to indicate the unfolding state of a primitive projection,

so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.

1 files changed, 19 insertions, 1 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index 49a838ae5..893cad09d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -634,7 +634,25 @@ val kn_ord : kernel_name -> kernel_name -> int
 type constant = Constant.t
 (** @deprecated Alias type *)
 
-type projection = constant
+module Projection : sig
+  type t
+    
+  val make : constant -> bool -> t
+
+  val constant : t -> constant
+  val unfolded : t -> bool
+  val unfold : t -> t
+
+  val equal : t -> t -> bool
+  val hash : t -> int
+  val hashcons : t -> t
+
+  val compare : t -> t -> int
+    
+  val map : (constant -> constant) -> t -> t
+end
+
+type projection = Projection.t
 
 val constant_of_kn_equiv : KerName.t -> KerName.t -> constant
 (** @deprecated Same as [Constant.make] *)