From 72c03f36e2e969992acf8e0398bbf7ae2c2c70b8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 20 Nov 2001 15:35:22 +0000
Subject: Fusion de declare/add_constant, declare/add_parameter et
 add_discharged_constant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/psyntax.ml4 | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'contrib')

diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index b85a50790f..77d2616532 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -546,9 +546,11 @@ let _ =
 	      let ren = update empty_ren "" [] in
 	      let v = Ptyping.cic_type_v env ren v in
 	      if not (is_mutable v) then begin
-		let c = trad_ml_type_v ren env v in
+		let c =
+		  Safe_typing.ParameterEntry (trad_ml_type_v ren env v),
+		  Declare.NeverDischarge in
 		List.iter 
-		  (fun id -> ignore (Declare.declare_parameter id c)) ids;
+		  (fun id -> ignore (Declare.declare_constant id c)) ids;
 		if_verbose (is_assumed false) ids
 	      end;
 	      if not (is_pure v) then begin
-- 
cgit v1.2.3