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

1 files changed, 4 insertions, 2 deletions

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