diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 7 | ||||
| -rw-r--r-- | toplevel/command.ml | 3 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 8 |
3 files changed, 4 insertions, 14 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 561175013..8ffb08c55 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -69,11 +69,6 @@ let rec stre_unif_cond = function and stre2 = (variable_strength v2) in stre_max (stre1,stre2) -let stre_of_global = function - | ConstRef sp -> constant_or_parameter_strength sp - | VarRef id -> variable_strength id - | IndRef _ | ConstructRef _ -> NeverDischarge - (* Errors *) type coercion_error_kind = @@ -235,7 +230,7 @@ let prods_of t = let get_strength stre ref cls clt = let stres = (snd (class_info cls)).cl_strength in let stret = (snd (class_info clt)).cl_strength in - let stref = stre_of_global ref in + let stref = strength_of_global ref in (* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ? let streunif = stre_unif_cond (s_vardep,f_vardep) in *) diff --git a/toplevel/command.ml b/toplevel/command.ml index 5906d7520..0ff52efda 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 diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index a6fbb7283..4c5e21b0a 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -170,7 +170,6 @@ type opacity = bool type discharge_operation = | Variable of identifier * section_variable_entry * strength * bool - | Parameter of identifier * constr * bool | Constant of section_path * recipe * strength * bool | Inductive of mutual_inductive_entry * bool | Class of cl_typ * cl_info_typ @@ -215,7 +214,7 @@ let process_object oldenv dir sec_sp | ("CONSTANT" | "PARAMETER") -> (* CONSTANT/PARAMETER means never discharge (though visibility *) (* may vary) *) - let stre = constant_or_parameter_strength sp in + let stre = constant_strength sp in (* if stre = (DischargeAt sec_sp) then let cb = Environ.lookup_constant sp oldenv in @@ -294,11 +293,8 @@ let process_operation = function let _ = with_implicits imp (declare_variable id) (Lib.cwd(),expmod_a,stre) in () - | Parameter (spid,typ,imp) -> - let _ = with_implicits imp (declare_parameter spid) typ in - constant_message spid | Constant (sp,r,stre,imp) -> - with_implicits imp (redeclare_constant sp) (ConstantRecipe r,stre); + with_implicits imp (redeclare_constant sp) (r,stre); constant_message (basename sp) | Inductive (mie,imp) -> let _ = with_implicits imp declare_mind mie in |