From ba268db78c86f9ca0ccdb2524193e5346f7155b3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Dec 2002 09:54:38 +0000
Subject: Déplacement du hash-consing vers declare.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3412 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 88de140dfa..31dd7e08a0 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -444,6 +444,9 @@ and execute_list env l cu =
 let infer env constr =
   let (j,(cst,_)) =
     execute env constr (Constraint.empty, universes env) in
+  let j = if j.uj_val = constr then { j with uj_val = constr } else
+    (error "Kernel built a body different from its input\n";
+     flush stdout; j) in
   (j, cst)
 
 let infer_type env constr =
-- 
cgit v1.2.3