From 8ff2de8c01b3ba3563517627b1f5c9eb2c4bcb77 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 14 Mar 2012 09:53:06 +0000
Subject: Final part of moving Program code inside the main code. Adapted
 add_definition/fixpoint and parsing of the "Program" prefix.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.ml  | 1 +
 kernel/environ.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index c38d4186fb..15babb2ab8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -100,6 +100,7 @@ let map_named_val f (ctxt,ctxtv) =
 let empty_named_context = empty_named_context
 
 let push_named = push_named
+let push_named_context = List.fold_right push_named
 let push_named_context_val = push_named_context_val
 
 let val_of_named_context ctxt =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 42100e4eb9..70369ae4ca 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -81,6 +81,7 @@ val map_named_val :
    (constr -> constr) -> named_context_val -> named_context_val
 
 val push_named : named_declaration -> env -> env
+val push_named_context : named_context -> env -> env
 val push_named_context_val  :
     named_declaration -> named_context_val -> named_context_val
 
-- 
cgit v1.2.3