diff options
| author | filliatr | 1999-12-08 15:15:47 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-08 15:15:47 +0000 |
| commit | c4dccc430e10b784e65b5bf3330c55d658d2883d (patch) | |
| tree | 42afd0f7ff5f3c2079f65597fe15f46a1b830203 /toplevel/command.ml | |
| parent | b3e6d156fbc13ae6d79075265fc20f8912c520da (diff) | |
deplacement de Discharge dans toplevel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 217acdb0a1..882033919d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -40,7 +40,7 @@ let constant_entry_of_com com = let definition_body ident n com = let ce = constant_entry_of_com com in - declare_constant ident (ce,n,false) + declare_constant ident (ce,n) let red_constant_entry ce = function | None -> ce @@ -53,7 +53,7 @@ let red_constant_entry ce = function let definition_body_red ident n com red_option = let ce = constant_entry_of_com com in let ce' = red_constant_entry ce red_option in - declare_constant ident (ce',n,false) + declare_constant ident (ce',n) let syntax_definition ident com = let c = raw_constr_of_com Evd.empty (Global.context()) com in @@ -236,7 +236,7 @@ let build_recursive lnameargsardef = let ce = { const_entry_body = mkFixDlam (Array.of_list nvrec) i varrec recvec; const_entry_type = None } in - declare_constant fi (ce, n, false); + declare_constant fi (ce, n); declare (i+1) lf | _ -> () in @@ -251,7 +251,7 @@ let build_recursive lnameargsardef = (fun subst (f,def) -> let ce = { const_entry_body = Generic.replace_vars subst def; const_entry_type = None } in - declare_constant f (ce,n,false); + declare_constant f (ce,n); warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst lnamerec) @@ -300,7 +300,7 @@ let build_corecursive lnameardef = let ce = { const_entry_body = mkCoFixDlam i (Array.of_list larrec) recvec; const_entry_type = None } in - declare_constant fi (ce,n,false); + declare_constant fi (ce,n); declare (i+1) lf | _ -> () in @@ -314,7 +314,7 @@ let build_corecursive lnameardef = (fun subst (f,def) -> let ce = { const_entry_body = Generic.replace_vars subst def; const_entry_type = None } in - declare_constant f (ce,n,false); + declare_constant f (ce,n); warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst lnamerec) @@ -338,7 +338,7 @@ let build_scheme lnamedepindsort = | fi::lf -> let ce = { const_entry_body = listdecl.(i); const_entry_type = None } in - declare_constant fi (ce,n,false); + declare_constant fi (ce,n); declare (i+1) lf | _ -> () in |