diff options
| author | herbelin | 2001-11-20 15:35:22 +0000 |
|---|---|---|
| committer | herbelin | 2001-11-20 15:35:22 +0000 |
| commit | 72c03f36e2e969992acf8e0398bbf7ae2c2c70b8 (patch) | |
| tree | 58f880037a6b24d23b770b427f07b6d03d93a81f /toplevel/command.ml | |
| parent | 52c0bf0da05bcfce49ce5c8321e8b9ed7b3a1cb5 (diff) | |
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 5906d75202..0ff52efdac 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -33,7 +33,6 @@ open Nametab open Typeops open Indtypes -let mkCastC(c,t) = ope("CAST",[c;t]) let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some x,b)]) let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)]) @@ -103,7 +102,7 @@ let syntax_definition ident com = let parameter_def_var ident c = let c = interp_type Evd.empty (Global.env()) c in - let sp = declare_parameter ident c in + let sp = declare_constant ident (ParameterEntry c, NeverDischarge) in if_verbose message ((string_of_id ident) ^ " is assumed"); sp |