From 54155675d0f5c724474d4bb6f16ca5f3fa60a6fe Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 19 Aug 2013 12:27:10 +0000
Subject: abstract+Defined: create opaque sub proofs (as pre-ParalITP)

Non-opaque-constant's side effects are processed before
the constant enters the kernel and global constants are
generated for them (as before, but not by side effect in
the middle of the proof construction).
This makes sense because proofs ending with Defined have
to be run immediately, so the list of side effects is
immediately available.

These side effects are type checked again.
To fix that the idea of kernel signatures could be employed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16702 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declareops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index b0f320942e..ac3aad15e7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -226,7 +226,7 @@ let string_of_side_effect = function
   | NewConstant (c,_) -> Names.string_of_con c
 type side_effects = side_effect list
 let no_seff = ([] : side_effects)
-let iter_side_effects f l = List.iter f l
+let iter_side_effects f l = List.iter f (List.rev l)
 let fold_side_effects f a l = List.fold_left f a l
 let uniquize_side_effects l = List.uniquize l
 let union_side_effects l1 l2 = l1 @ l2
-- 
cgit v1.2.3