diff options
| author | herbelin | 2000-11-09 16:37:10 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-09 16:37:10 +0000 |
| commit | 05f7dc09dea7f8ba949aeb8108f041a882fa4cf8 (patch) | |
| tree | cccf0e25701b4b8a9b995a982e64c9d495cf4bd7 /toplevel/command.ml | |
| parent | c60ee989404713617b7278ad26c285d8cea229fc (diff) | |
Renommage canonique SectionLocalDecl -> SectionLocalAssum
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@837 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 1a236c3ff7..cf980cc79b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -84,7 +84,7 @@ let hypothesis_def_var is_refining ident n c = if Lib.is_section_p disch_sp then begin let t = interp_type Evd.empty (Global.env()) c in declare_variable (id_of_string ident) - (SectionLocalDecl t,n,false); + (SectionLocalAssum t,n,false); if is_verbose() then message (ident ^ " is assumed"); if is_refining then mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; @@ -207,7 +207,7 @@ let build_recursive lnameargsardef = let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in let arity = arj.utj_val in declare_variable recname - (SectionLocalDecl arj.utj_val,NeverDischarge,false); + (SectionLocalAssum arj.utj_val,NeverDischarge,false); (Environ.push_named_assum (recname,arity) env, (arity::arl))) (env0,[]) lnameargsardef with e -> @@ -274,7 +274,7 @@ let build_corecursive lnameardef = let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in let arity = arj.utj_val in declare_variable recname - (SectionLocalDecl arj.utj_val,NeverDischarge,false); + (SectionLocalAssum arj.utj_val,NeverDischarge,false); (Environ.push_named_assum (recname,arity) env, (arity::arl))) (env0,[]) lnameardef with e -> |