aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/funind/tacinv.ml42
-rw-r--r--contrib/interface/name_to_ast.ml2
-rw-r--r--contrib/interface/xlate.ml21
-rw-r--r--contrib/recdef/recdef.ml410
-rw-r--r--contrib/subtac/rewrite.ml4
-rw-r--r--contrib/xml/xmlcommand.ml29
6 files changed, 25 insertions, 43 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index bf918ba560..c2410d55ca 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -842,7 +842,7 @@ let declareFunScheme f fname mutflist =
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = true } in
- let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition)) in
+ let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition Scheme)) in
()
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 50c8a0fa1a..b06ba1992d 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -140,7 +140,7 @@ let make_variable_ast name typ implicits =
let make_definition_ast name c typ implicits =
- VernacDefinition ((Global,Definition false), (dummy_loc,name), DefineBody ([], None,
+ VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None,
(constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
(fun _ _ -> ()))
::(implicits_to_ast_list implicits);;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ea7b521624..f17cb67b43 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1361,24 +1361,9 @@ let coerce_genarg_to_VARG x =
| ExtraArgType s -> xlate_error "Cannot treat extra generic arguments"
-let xlate_thm x = CT_thm (match x with
- | Theorem -> "Theorem"
- | Remark -> "Remark"
- | Lemma -> "Lemma"
- | Fact -> "Fact")
-
-
-let xlate_defn x = CT_defn (match x with
- | (Local, Definition _) -> "Local"
- | (Global, Definition true) -> "Boxed Definition"
- | (Global, Definition false) -> "Definition"
- | (Global, SubClass) -> "SubClass"
- | (Global, Coercion) -> "Coercion"
- | (Local, SubClass) -> "Local SubClass"
- | (Local, Coercion) -> "Local Coercion"
- | (Global,CanonicalStructure) -> "Canonical Structure"
- | (Local, CanonicalStructure) ->
- xlate_error "Local CanonicalStructure not parsed")
+let xlate_thm x = CT_thm (string_of_theorem_kind x)
+
+let xlate_defn k = CT_defn (string_of_definition_kind k)
let xlate_var x = CT_var (match x with
| (Global,Definitional) -> "Parameter"
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 2e62aa407e..32febb6fa2 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -694,7 +694,7 @@ let new_com_terminate fonctional_ref input_type relation_ast rec_arg_num
let (evmap, env) = Command.get_current_context() in
let (relation:constr)= interp_constr evmap env relation_ast in
(start_proof thm_name
- (IsGlobal (Proof Lemma)) (Environ.named_context_val env)
+ (Global, Proof Lemma) (Environ.named_context_val env)
(new_hyp_terminates fonctional_ref) hook;
by (new_whole_start fonctional_ref
input_type relation rec_arg_num ));;
@@ -762,7 +762,7 @@ let (value_f:constr list -> global_reference -> constr) =
in
understand Evd.empty (Global.env()) value;;
-let (declare_fun : identifier -> global_kind -> constr -> global_reference) =
+let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
fun f_id kind value ->
let ce = {const_entry_body = value;
const_entry_type = None;
@@ -770,7 +770,7 @@ let (declare_fun : identifier -> global_kind -> constr -> global_reference) =
const_entry_boxed = true} in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
-let (declare_f : identifier -> global_kind -> constr list -> global_reference -> global_reference) =
+let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) =
fun f_id kind input_type fterm_ref ->
declare_fun f_id kind (value_f input_type fterm_ref);;
@@ -943,7 +943,7 @@ let (com_eqn : identifier ->
let (evmap, env) = Command.get_current_context() in
let eq_constr = interp_constr evmap env eq in
let f_constr = (constr_of_reference f_ref) in
- (start_proof eq_name (IsGlobal (Proof Lemma))
+ (start_proof eq_name (Global, Proof Lemma)
(Environ.named_context_val env) eq_constr (fun _ _ -> ());
by
(start_equation f_ref terminate_ref
@@ -978,7 +978,7 @@ let recursive_definition f type_of_f r rec_arg_num eq =
let equation_id = add_suffix f "_equation" in
let functional_id = add_suffix f "_F" in
let term_id = add_suffix f "_terminate" in
- let functional_ref = declare_fun functional_id IsDefinition res in
+ let functional_ref = declare_fun functional_id (IsDefinition Definition) res in
let hook _ _ =
let term_ref = Nametab.locate (make_short_qualid term_id) in
let f_ref = declare_f f (IsProof Lemma) arg_types term_ref in
diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml
index 201f2d48b9..afbbd18af5 100644
--- a/contrib/subtac/rewrite.ml
+++ b/contrib/subtac/rewrite.ml
@@ -539,8 +539,8 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
in aux ctx t
-let global_kind : Decl_kinds.global_kind = Decl_kinds.IsDefinition
-let goal_kind = Decl_kinds.IsGlobal Decl_kinds.DefinitionBody
+let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
+let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
let make_fixpoint t id term =
let term' = mkLambda (Name id, t.f_fulltype, term) in
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 96f73abe0e..39a12a7ea7 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -434,16 +434,10 @@ let theory_output_string ?(do_not_quote = false) s =
Buffer.add_string theory_buffer s
;;
-let kind_of_theorem = function
- | Decl_kinds.Theorem -> "Theorem"
- | Decl_kinds.Lemma -> "Lemma"
- | Decl_kinds.Fact -> "Fact"
- | Decl_kinds.Remark -> "Remark"
-
let kind_of_global_goal = function
- | Decl_kinds.IsGlobal Decl_kinds.DefinitionBody -> "DEFINITION","InteractiveDefinition"
- | Decl_kinds.IsGlobal (Decl_kinds.Proof k) -> "THEOREM",kind_of_theorem k
- | Decl_kinds.IsLocal -> assert false
+ | Decl_kinds.Global, Decl_kinds.DefinitionBody _ -> "DEFINITION","InteractiveDefinition"
+ | Decl_kinds.Global, (Decl_kinds.Proof k) -> "THEOREM",Decl_kinds.string_of_theorem_kind k
+ | Decl_kinds.Local, _ -> assert false
let kind_of_inductive isrecord kn =
"DEFINITION",
@@ -458,8 +452,9 @@ let kind_of_variable id =
| DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption"
| DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis"
| DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
- | DK.IsDefinition -> "VARIABLE","LocalDefinition"
- | DK.IsProof DK.LocalStatement -> "VARIABLE","LocalFact"
+ | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition"
+ | DK.IsProof _ -> "VARIABLE","LocalFact"
+ | _ -> Util.anomaly "Unsupported variable kind"
;;
let kind_of_constant kn =
@@ -468,8 +463,10 @@ let kind_of_constant kn =
| DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
| DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
| DK.IsAssumption DK.Conjectural -> "AXIOM","Conjecture"
- | DK.IsDefinition -> "DEFINITION","Definition"
- | DK.IsProof thm -> "THEOREM",kind_of_theorem thm
+ | DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
+ | DK.IsDefinition DK.Example -> "DEFINITION","Example"
+ | DK.IsDefinition _ -> Util.anomaly "Unsupported constant kind"
+ | DK.IsProof thm -> "THEOREM",DK.string_of_theorem_kind thm
;;
let kind_of_global r =
@@ -560,10 +557,10 @@ let show_pftreestate internal fn (kind,pftst) id =
let kn = Lib.make_kn id in
let env = Global.env () in
let obj =
- mk_current_proof_obj (kind = Decl_kinds.IsLocal) id val0 typ evar_map env in
+ mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in
let uri =
match kind with
- Decl_kinds.IsLocal ->
+ Decl_kinds.Local, _ ->
let uri =
"cic:/" ^ String.concat "/"
(Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable)
@@ -571,7 +568,7 @@ let show_pftreestate internal fn (kind,pftst) id =
let kind_of_var = "VARIABLE","LocalFact" in
if not internal then print_object_kind uri kind_of_var;
uri
- | Decl_kinds.IsGlobal _ ->
+ | Decl_kinds.Global, _ ->
let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in
if not internal then print_object_kind uri (kind_of_global_goal kind);
uri
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 02:31:53 +0000