From 99fe89385f6590aac5bc2dadf246c3d021986f7c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 May 2017 18:08:24 +0200
Subject: Using EConstr and more invariants in record.ml.

---
 engine/eConstr.ml  | 2 ++
 engine/eConstr.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c0485e4e76..1f4ff5092f 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -45,6 +45,7 @@ val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t,
 val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
 val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
 val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt
+val to_rel_decl : Evd.evar_map -> (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
 end =
 struct
 
@@ -131,6 +132,7 @@ let of_named_decl d = d
 let unsafe_to_named_decl d = d
 let of_rel_decl d = d
 let unsafe_to_rel_decl d = d
+let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
 
 end
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9d705b4d55..06020c5738 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -266,6 +266,8 @@ val fresh_global :
 val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
 val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt
 
+val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
+
 (** {5 Unsafe operations} *)
 
 module Unsafe :
-- 
cgit v1.2.3