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 /kernel/cooking.mli | |
| 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 'kernel/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 48f4dfc83..3cd03fc9a 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -16,17 +16,15 @@ open Univ (*s Cooking the constants. *) -type modification_action = ABSTRACT | ERASE - type 'a modification = | NOT_OCCUR - | DO_ABSTRACT of 'a * modification_action list + | DO_ABSTRACT of 'a * constr array | DO_REPLACE of constant_body type work_list = - (section_path * section_path modification) list - * (inductive_path * inductive_path modification) list - * (constructor_path * constructor_path modification) list + (constant * constant modification) list + * (inductive * inductive modification) list + * (constructor * constructor modification) list type recipe = { d_from : constant_body; @@ -38,7 +36,7 @@ val cook_constant : (*s Utility functions used in module [Discharge]. *) -val expmod_constr : env -> work_list -> constr -> constr -val expmod_type : env -> work_list -> types -> types +val expmod_constr : work_list -> constr -> constr +val expmod_type : work_list -> types -> types |