From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Oct 2016 17:53:07 +0100
Subject: Termops API using EConstr.

---
 pretyping/recordops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index a6a90c751b..4a176760c2 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -65,7 +65,7 @@ type obj_typ = {
   o_TCOMPS : constr list } (** ordered *)
 
 (** Return the form of the component of a canonical structure *)
-val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
+val cs_pattern_of_constr : Evd.evar_map -> constr -> cs_pattern * int option * constr list
 
 val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 
-- 
cgit v1.2.3


From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Nov 2016 20:53:32 +0100
Subject: Reductionops API using EConstr.

---
 pretyping/recordops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 4a176760c2..405963a9ca 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -72,6 +72,6 @@ val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
 val declare_canonical_structure : global_reference -> unit
 val is_open_canonical_projection :
-  Environ.env -> Evd.evar_map -> (constr * constr Reductionops.Stack.t) -> bool
+  Environ.env -> Evd.evar_map -> Reductionops.state -> bool
 val canonical_projections : unit ->
   ((global_reference * cs_pattern) * obj_typ) list
-- 
cgit v1.2.3


From b113f9e1ca88514cd9d94dfe90669a27689b7434 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 03:11:44 +0100
Subject: Recordops API using EConstr.

---
 pretyping/recordops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 405963a9ca..7c0d0ec6d4 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -65,7 +65,7 @@ type obj_typ = {
   o_TCOMPS : constr list } (** ordered *)
 
 (** Return the form of the component of a canonical structure *)
-val cs_pattern_of_constr : Evd.evar_map -> constr -> cs_pattern * int option * constr list
+val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
 
 val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 
-- 
cgit v1.2.3