From 63dcece33905126da8823d7ac048dce1b1454205 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 10 Jun 2003 20:55:45 +0000 Subject: code mort git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4107 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/impargs.ml | 18 ------------------ 1 file changed, 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 -- cgit v1.2.3