diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-09 16:40:03 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-09 16:40:03 +0000 |
| commit | f1778f0e830c50aaec250916f14e202d95960414 (patch) | |
| tree | ae220556180dfa55d6b638467deb7edf58d4c17b /library/impargs.ml | |
| parent | 8dbab7f463cabfc2913ab8615973c96ac98bf371 (diff) | |
Suppression des arguments sur les constantes, inductifs et constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index d71acd70f..63351392e 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -126,7 +126,7 @@ let constant_implicits_list sp = implicit arguments of the constructors. *) module Inductive_path = struct - type t = inductive_path + type t = inductive let compare (spx,ix) (spy,iy) = let c = ix - iy in if c = 0 then sp_ord spx spy else c end @@ -136,7 +136,7 @@ module Indmap = Map.Make(Inductive_path) let inductives_table = ref Indmap.empty module Construtor_path = struct - type t = constructor_path + 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 @@ -269,18 +269,15 @@ let context_of_global_reference = function | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps let type_of_global r = - let args = - Array.of_list - (Sign.instance_from_section_context (context_of_global_reference r)) in match r with | VarRef sp -> lookup_named_type (basename sp) (Global.env ()) | ConstRef sp -> - Typeops.type_of_constant (Global.env ()) Evd.empty (sp,args) + Typeops.type_of_constant (Global.env ()) Evd.empty sp | IndRef sp -> - Typeops.type_of_inductive (Global.env ()) Evd.empty (sp,args) + Typeops.type_of_inductive (Global.env ()) Evd.empty sp | ConstructRef sp -> - Typeops.type_of_constructor (Global.env ()) Evd.empty (sp,args) + Typeops.type_of_constructor (Global.env ()) Evd.empty sp let check_range n i = if i<1 or i>n then error ("Bad argument number: "^(string_of_int i)) |