diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-14 15:41:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-14 15:41:55 +0000 |
| commit | e7d592ada2d681876d2bcf0a45d4267b3746064f (patch) | |
| tree | e0b7eb1e67b1871b7cb356c33f66182f6dde86c3 /library/global.ml | |
| parent | 045c85f66a65c6aaedeed578d352c6de27d5e6a4 (diff) | |
Mise en place d'un système optionnel de discharge immédiat; prise en compte des défs locales dans les arguments des inductifs; nettoyage divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/library/global.ml b/library/global.ml index e5f0d07fd..c07452988 100644 --- a/library/global.ml +++ b/library/global.ml @@ -35,11 +35,11 @@ let named_context () = named_context !global_env let push_named_def idc = global_env := push_named_def idc !global_env let push_named_assum idc = global_env := push_named_assum idc !global_env -let add_parameter sp c = global_env := add_parameter sp c !global_env -let add_constant sp ce = global_env := add_constant sp ce !global_env -let add_discharged_constant sp r = - global_env := add_discharged_constant sp r !global_env -let add_mind sp mie = global_env := add_mind sp mie !global_env +let add_parameter sp c l = global_env := add_parameter sp c l !global_env +let add_constant sp ce l = global_env := add_constant sp ce l !global_env +let add_discharged_constant sp r l = + global_env := add_discharged_constant sp r l !global_env +let add_mind sp mie l = global_env := add_mind sp mie l !global_env let add_constraints c = global_env := add_constraints c !global_env let pop_named_decls ids = global_env := pop_named_decls ids !global_env @@ -87,8 +87,6 @@ let mind_is_recursive = let mind_nconstr = Util.compose Inductive.mis_nconstr lookup_mind_specif let mind_nparams = Util.compose Inductive.mis_nparams lookup_mind_specif -let mind_nf_arity x = - body_of_type (Inductive.mis_user_arity (lookup_mind_specif x)) let mind_nf_lc = Util.compose Inductive.mis_nf_lc lookup_mind_specif |