diff options
| author | sacerdot | 2004-11-16 12:37:40 +0000 |
|---|---|---|
| committer | sacerdot | 2004-11-16 12:37:40 +0000 |
| commit | d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (patch) | |
| tree | ed4d954a685588ee55f4d8902eba8a1afc864472 /library/impargs.ml | |
| parent | 08cb37edb71af0301a72acc834d50f24b0733db5 (diff) | |
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
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 5bf920014b..d775433673 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -289,7 +289,7 @@ let list_of_implicits = function (*s Constants. *) -let constants_table = ref KNmap.empty +let constants_table = ref Cmap.empty let compute_constant_implicits kn = let env = Global.env () in @@ -297,7 +297,7 @@ let compute_constant_implicits kn = auto_implicits env (body_of_type cb.const_type) let constant_implicits sp = - try KNmap.find sp !constants_table with Not_found -> No_impl,No_impl + try Cmap.find sp !constants_table with Not_found -> No_impl,No_impl (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where @@ -349,7 +349,7 @@ let cache_implicits_decl (r,imps) = | VarRef id -> var_table := Idmap.add id imps !var_table | ConstRef kn -> - constants_table := KNmap.add kn imps !constants_table + constants_table := Cmap.add kn imps !constants_table | IndRef indp -> inductives_table := Indmap.add indp imps !inductives_table; | ConstructRef consp -> @@ -485,7 +485,7 @@ let test_if_implicit find a = with Not_found -> (false,false,false),(false,false,false) let is_implicit_constant sp = - test_if_implicit (KNmap.find sp) !constants_table + test_if_implicit (Cmap.find sp) !constants_table let is_implicit_inductive_definition indp = test_if_implicit (Indmap.find (indp,0)) !inductives_table @@ -496,7 +496,7 @@ let is_implicit_var id = (*s Registration as global tables *) let init () = - constants_table := KNmap.empty; + constants_table := Cmap.empty; inductives_table := Indmap.empty; constructors_table := Constrmap.empty; var_table := Idmap.empty |