aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2003-06-10 20:55:45 +0000
committerherbelin2003-06-10 20:55:45 +0000
commit63dcece33905126da8823d7ac048dce1b1454205 (patch)
treeebcb338d44dda6389609622a369f2b0252b8fed1
parent05b125d1855a127fa829ba13c76aa91eed590a3c (diff)
code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4107 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--library/impargs.ml18
1 files changed, 0 insertions, 18 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index 420188d356..38267c3c8e 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -298,24 +298,6 @@ let constant_implicits sp =
$i$ are the implicit arguments of the inductive and $v$ the array of
implicit arguments of the constructors. *)
-module Inductive_path = struct
- type t = inductive
- let compare (spx,ix) (spy,iy) =
- let c = ix - iy in if c = 0 then compare spx spy else c
-end
-
-module Indmap = Map.Make(Inductive_path)
-
-let inductives_table = ref Indmap.empty
-
-module Construtor_path = struct
- type t = constructor
- let compare (indx,ix) (indy,iy) =
- let c = ix - iy in if c = 0 then Inductive_path.compare indx indy else c
-end
-
-module Constrmap = Map.Make(Construtor_path)
-
let inductives_table = ref Indmap.empty
let constructors_table = ref Constrmap.empty