aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/extraction/common.ml2
-rw-r--r--contrib/interface/centaur.ml42
-rw-r--r--contrib/interface/name_to_ast.ml2
-rw-r--r--contrib/xml/xmlcommand.ml7
-rw-r--r--contrib/xml/xmlcommand.ml47
-rw-r--r--parsing/prettyp.ml4
-rw-r--r--parsing/search.ml3
-rw-r--r--toplevel/discharge.ml5
8 files changed, 12 insertions, 20 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 811591bd8..5d82bad51 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -106,7 +106,7 @@ let extract_module m =
let get_reference = function
| (_,kn), Leaf o ->
(match Libobject.object_tag o with
- | "CONSTANT" | "PARAMETER" -> ConstRef kn
+ | "CONSTANT" -> ConstRef kn
| "INDUCTIVE" -> IndRef (kn,0)
| _ -> failwith "caught")
| _ -> failwith "caught"
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index ded82a691..fd8d64f07 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -414,7 +414,7 @@ let inspect n =
(sp,_), "VARIABLE" ->
let (_, _, v) = get_variable (basename sp) in
add_search2 (Nametab.locate (qualid_of_sp sp)) v
- | (sp,kn), ("CONSTANT"|"PARAMETER") ->
+ | (sp,kn), "CONSTANT" ->
let {const_type=typ} = Global.lookup_constant kn in
add_search2 (Nametab.locate (qualid_of_sp sp)) typ
| (sp,kn), "MUTUALINDUCTIVE" ->
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index a7e1f3444..80009d783 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -205,7 +205,7 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
let tag = object_tag lobj in
match tag with
| "VARIABLE" -> variable_to_ast_list (basename sp)
- | "CONSTANT"|"PARAMETER" -> constant_to_ast_list kn
+ | "CONSTANT" -> constant_to_ast_list kn
| "INDUCTIVE" -> inductive_to_ast_list kn
| s ->
errorlabstrm
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 07df70a0c..b05b7baa8 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -32,8 +32,7 @@ exception Uninteresting;;
(*CSC: CODE USEFUL ONLY FOR THE CODE COMMENTED OUT
let tag_of_string_tag =
function
- "CONSTANT"
- | "PARAMETER" -> Constant
+ "CONSTANT" -> Constant
| "INDUCTIVE" -> Inductive
| "VARIABLE" -> Variable
| _ -> raise Uninteresting
@@ -76,7 +75,6 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *)
| DK.Local -> false (* a local definition *)
| DK.Global -> true (* a non-local one *)
)
- | "PARAMETER" (* axioms and *)
| "INDUCTIVE" -> true (* mutual inductive types are never local *)
| "VARIABLE" -> false (* variables are local, so no namesakes *)
| _ -> false (* uninteresting thing that won't be printed*)
@@ -541,8 +539,7 @@ let print_coq_object lobj id sp dn fv env =
let tag = tag_of_string_tag strtag in
let obj =
match strtag with
- "CONSTANT" (* = Definition, Theorem *)
- | "PARAMETER" (* = Axiom *) ->
+ "CONSTANT" (* = Definition, Theorem, Axiom *)
let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
G.lookup_constant sp
in
diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index 5ca89dd3f..3aaf77615 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -38,8 +38,7 @@ exception Uninteresting;;
let tag_of_string_tag =
function
- "CONSTANT"
- | "PARAMETER" -> Constant
+ "CONSTANT" -> Constant
| "INDUCTIVE" -> Inductive
| "VARIABLE" -> Variable
| _ -> raise Uninteresting
@@ -89,7 +88,6 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *)
| L.NotDeclare -> false (* not a definition *)
| L.NeverDischarge -> true (* a non-local one *)
)
- | "PARAMETER" (* axioms and *)
| "INDUCTIVE" -> true (* mutual inductive types are never local *)
| "VARIABLE" -> false (* variables are local, so no namesakes *)
| _ -> false (* uninteresting thing that won't be printed*)
@@ -848,8 +846,7 @@ let print_object lobj id (sp,kn) dn fv env =
let inner_types = ref [] in
let pp_cmds =
match strtag with
- "CONSTANT" (* = Definition, Theorem *)
- | "PARAMETER" (* = Axiom *) ->
+ "CONSTANT" -> (* = Definition, Theorem, Axiom *)
let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
G.lookup_constant kn
in
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index efcb5c8af..4621f1bb2 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -313,7 +313,7 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
match (oname,tag) with
| (_,"VARIABLE") ->
print_section_variable (basename sp) ++ fnl ()
- | (_,("CONSTANT"|"PARAMETER")) ->
+ | (_,"CONSTANT") ->
print_constant with_values sep kn ++ fnl ()
| (_,"INDUCTIVE") ->
print_inductive kn ++ fnl ()
@@ -504,7 +504,7 @@ let print_local_context () =
and print_last_const = function
| (oname,Lib.Leaf lobj)::rest ->
(match object_tag lobj with
- | "CONSTANT" | "PARAMETER" ->
+ | "CONSTANT" ->
let kn = snd oname in
let {const_body=val_0;const_type=typ} =
Global.lookup_constant kn in
diff --git a/parsing/search.ml b/parsing/search.ml
index c771a7737..c1e897fd0 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -58,8 +58,7 @@ let crible (fn : global_reference -> env -> constr -> unit) ref =
let (idc,_,typ) = get_variable (basename sp) in
if (head_const typ) = const then fn (VarRef idc) env typ
with Not_found -> (* we are in a section *) ())
- | "CONSTANT"
- | "PARAMETER" ->
+ | "CONSTANT" ->
let kn=locate_constant (qualid_of_sp sp) in
let {const_type=typ} = Global.lookup_constant kn in
if (head_const typ) = const then fn (ConstRef kn) env typ
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index a58d20ad6..f3c4b68b3 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -209,9 +209,8 @@ let process_object oldenv olddir full_olddir newdir
(* always discharged *)
(Constraints cst :: ops, id :: ids_to_discard, work_alist)
- | ("CONSTANT" | "PARAMETER") ->
- (* CONSTANT/PARAMETER means never discharge (though visibility *)
- (* may vary) *)
+ | "CONSTANT" ->
+ (* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 12:11:15 +0000