aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/class.ml20
-rw-r--r--toplevel/command.ml18
-rw-r--r--toplevel/discharge.ml12
-rw-r--r--toplevel/metasyntax.ml2
-rw-r--r--toplevel/record.ml6
5 files changed, 33 insertions, 25 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 3d468d3281..c9ed58c795 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -150,7 +150,7 @@ let uniform_cond nargs lt =
let id_of_cl = function
| CL_FUN -> id_of_string "FUNCLASS"
| CL_SORT -> id_of_string "SORTCLASS"
- | CL_CONST kn -> id_of_label (label kn)
+ | CL_CONST kn -> id_of_label (con_label kn)
| CL_IND ind ->
let (_,mip) = Global.lookup_inductive ind in
mip.mind_typename
@@ -271,7 +271,7 @@ let build_id_coercion idf_opt source =
const_entry_type = Some typ_f;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()} in
- let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
+ let kn = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
ConstRef kn
let check_source = function
@@ -390,13 +390,17 @@ let defined_in_sec kn olddir =
let _,dir,_ = repr_kn kn in
dir = olddir
+let con_defined_in_sec kn olddir =
+ let _,dir,_ = repr_con kn in
+ dir = olddir
+
(* This moves the global path one step below *)
let process_global olddir = function
| VarRef _ ->
anomaly "process_global only processes global surviving the section"
| ConstRef kn as x ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
+ if con_defined_in_sec kn olddir then
+ let newkn = Lib.make_con (id_of_label (con_label kn)) in
ConstRef newkn
else x
| IndRef (kn,i) as x ->
@@ -416,8 +420,8 @@ let process_class olddir ids_to_discard x =
match cl with
| CL_SECVAR _ -> x
| CL_CONST kn ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
+ if con_defined_in_sec kn olddir then
+ let newkn = Lib.make_con (id_of_label (con_label kn)) in
let hyps = (Global.lookup_constant kn).const_hyps in
let n = count_extra_abstractions hyps ids_to_discard in
(CL_CONST newkn,{cl_strength=stre;cl_param=p+n})
@@ -437,8 +441,8 @@ let process_cl sec_sp cl =
match cl with
| CL_SECVAR id -> cl
| CL_CONST kn ->
- if defined_in_sec kn sec_sp then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
+ if con_defined_in_sec kn sec_sp then
+ let newkn = Lib.make_con (id_of_label (con_label kn)) in
CL_CONST newkn
else
cl
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8eaab89d34..a17d446660 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -113,7 +113,7 @@ let red_constant_entry ce = function
reduction_of_redexp red (Global.env()) Evd.empty body }
let declare_global_definition ident ce local =
- let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in
+ let kn = declare_constant ident (DefinitionEntry ce,IsDefinition) in
if local = Local then
msg_warning (pr_id ident ++ str" is declared as a global definition");
definition_message ident;
@@ -166,7 +166,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
str" is not visible from current goals");
VarRef ident
| (Global|Local) ->
- let (_,kn) =
+ let kn =
declare_constant ident (ParameterEntry c, IsAssumption kind) in
assumption_message ident;
if local=Local & Options.is_verbose () then
@@ -215,7 +215,7 @@ let declare_one_elimination ind =
if List.mem InType kelim then
let elim = make_elim (new_sort_in_family InType) in
let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in
- let c = mkConst (snd cte) and t = constant_type (Global.env()) (snd cte) in
+ let c = mkConst cte and t = constant_type (Global.env()) cte in
List.iter (fun (sort,suff) ->
let (t',c') =
Indrec.instanciate_type_indrec_scheme (new_sort_in_family sort)
@@ -514,7 +514,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
const_entry_type = Some arrec.(i);
const_entry_opaque = false;
const_entry_boxed = boxed} in
- let (_,kn) = declare_constant fi (DefinitionEntry ce, IsDefinition) in
+ let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
(ConstRef kn)
in
(* declare the recursive definitions *)
@@ -581,7 +581,7 @@ let build_corecursive lnameardef boxed =
const_entry_opaque = false;
const_entry_boxed = boxed }
in
- let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
+ let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
(ConstRef kn)
in
let lrefrec = Array.mapi declare namerec in
@@ -621,7 +621,7 @@ let build_scheme lnamedepindsort =
const_entry_type = Some decltype;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions() } in
- let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
+ let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
ConstRef kn :: lrecref
in
let lrecref = List.fold_right2 declare listdecl lrecnames [] in
@@ -666,11 +666,11 @@ let save id const kind hook =
(Local, VarRef id)
| IsLocal ->
let k = IsDefinition in
- let _,kn = declare_constant id (DefinitionEntry const, k) in
+ let kn = declare_constant id (DefinitionEntry const, k) in
(Global, ConstRef kn)
| IsGlobal k ->
let k = theorem_kind_of_goal_kind k in
- let _,kn = declare_constant id (DefinitionEntry const, k) in
+ let kn = declare_constant id (DefinitionEntry const, k) in
(Global, ConstRef kn) in
hook l r;
Pfedit.delete_current_proof ();
@@ -707,7 +707,7 @@ let admit () =
if k <> IsGlobal (Proof Conjecture) then
error "Only statements declared as conjecture can be admitted";
*)
- let (_,kn) =
+ let kn =
declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in
hook Global (ConstRef kn);
Pfedit.delete_current_proof ();
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b1ba1f7480..443fd61e1a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -41,6 +41,10 @@ let recalc_kn dir kn =
let (mp,_,l) = Names.repr_kn kn in
Names.make_kn mp dir l
+let recalc_con dir con =
+ let (mp,_,l) = Names.repr_con con in
+ Names.make_con mp dir l
+
let rec find_var id = function
| [] -> false
| (x,b,_)::l -> if x = id then b=None else find_var id l
@@ -214,10 +218,10 @@ let process_object oldenv olddir full_olddir newdir
(* CONSTANT means never discharge (though visibility may vary) *)
let kind = constant_kind sp in
let kn = Nametab.locate_constant (qualid_of_sp sp) in
- let lab = label kn in
+ let lab = con_label kn in
let cb = Environ.lookup_constant kn oldenv in
let imp = is_implicit_constant kn in
- let newkn = recalc_kn newdir kn in
+ let newkn = recalc_con newdir kn in
let abs_vars,discharged_hyps0 =
build_abstract_list full_olddir cb.const_hyps ids_to_discard in
(* let's add the new discharged hypothesis to those already discharged*)
@@ -268,12 +272,12 @@ let process_object oldenv olddir full_olddir newdir
let mib = Environ.lookup_mind newkn (Global.env ()) in
{ s_CONST = info.s_CONST;
s_PARAM = mib.mind_packets.(0).mind_nparams;
- s_PROJ = List.map (option_app (fun kn -> recalc_kn newdir kn)) info.s_PROJ } in
+ s_PROJ = List.map (option_app (fun kn -> recalc_con newdir kn)) info.s_PROJ } in
((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist)
| "OBJDEF1" ->
let kn = outObjDef1 lobj in
- let new_kn = recalc_kn newdir kn in
+ let new_kn = recalc_con newdir kn in
((Objdef new_kn)::ops, ids_to_discard, work_alist)
| "REQUIRE" ->
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index bc037f851b..de6778291f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1110,7 +1110,7 @@ let rec reify_meta_ast vars = function
Smetalam (loc,string_of_id id,reify_meta_ast vars body)
| Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast vars body)
| Nvar (loc,id) when List.mem id vars -> Nmeta (loc,string_of_id id)
- | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a
+ | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ | ConPath _ as a -> a
| Dynamic _ as a -> (* Hum... what to do here *) a
(* For old ast syntax *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 91f5b4ad88..ee189377d7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -176,7 +176,7 @@ let declare_projections indsp coers fields =
it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
- let (sp,kn) =
+ let kn =
try
let cie = {
const_entry_body = proj;
@@ -184,9 +184,9 @@ let declare_projections indsp coers fields =
const_entry_opaque = false;
const_entry_boxed = false } in
let k = (DefinitionEntry cie,IsDefinition) in
- let sp = declare_internal_constant fid k in
+ let kn = declare_internal_constant fid k in
Options.if_verbose message (string_of_id fid ^" is defined");
- sp
+ kn
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
let refi = ConstRef kn in
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-08 03:54:40 +0000