From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 10 Nov 2016 11:39:27 +0100
Subject: Unification API using EConstr.

---
 plugins/extraction/extraction.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 42a8cac69..0c4fa7055 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -99,6 +99,9 @@ let is_info_scheme env t = match flag_of_type env t with
 | (Info, TypeScheme) -> true
 | _ -> false
 
+let push_rel_assum (n, t) env =
+  Environ.push_rel (LocalAssum (n, t)) env
+
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
 let rec type_sign env c =
-- 
cgit v1.2.3