From d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Tue, 16 Nov 2004 12:37:40 +0000
Subject: IMPORTANT COMMIT: constant is now an ADT (it used to be equal to
 kernel_name).

MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.

KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/first-order/ground.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'contrib/first-order')

diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 418e6ce831..00a2260c6f 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -45,17 +45,17 @@ let update_flags ()=
 *)
 
 let update_flags ()=
-  let predref=ref Names.KNpred.empty in
+  let predref=ref Names.Cpred.empty in
   let f coe=
     try
       let kn=destConst (Classops.get_coercion_value coe) in
-	predref:=Names.KNpred.add kn !predref
+	predref:=Names.Cpred.add kn !predref
     with Invalid_argument "destConst"-> () in
     List.iter f (Classops.coercions ());
     red_flags:=
     Closure.RedFlags.red_add_transparent 
       Closure.betaiotazeta 
-      (Names.Idpred.full,Names.KNpred.complement !predref)
+      (Names.Idpred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
   update_flags ();
-- 
cgit v1.2.3