diff options
| -rw-r--r-- | kernel/term.ml | 66 | ||||
| -rw-r--r-- | kernel/term.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 11 |
3 files changed, 0 insertions, 79 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 111bcfbf3c..a83a8c6f23 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1307,21 +1307,6 @@ let rec occur_meta = function | DOP0(Meta(_)) -> true | _ -> false -(*Returns the maximum of metas. Returns -1 if there is no meta*) -(*let rec max_occur_meta=function - DOP2(Prod,t,DLAM(_,c)) -> - max (max_occur_meta t) (max_occur_meta c) - |DOP2(Lambda,t,DLAM(_,c)) -> - max (max_occur_meta t) (max_occur_meta c) - |DOPN(_,cl) -> - (try - List.hd (Sort.list (>) (List.map max_occur_meta (Array.to_list cl))) - with - Failure "hd" -> -1) - |DOP2(Cast,c,t) -> max (max_occur_meta c) (max_occur_meta t) - |DOP0(Meta n) -> n - |_ -> -1;;*) - let rel_vect = (Generic.rel_vect : int -> int -> constr array) let occur_existential = @@ -1599,54 +1584,3 @@ let sub_term_with_unif cref ceq= None else Some ((subst_with_lmeta l ceq),nb) - -let constr_display csr= - let rec term_display=function - DOP0(a) -> "DOP0("^(oper_display a)^")" - |DOP1(a,b) -> "DOP1("^(oper_display a)^","^(term_display b)^")" - |DOP2(a,b,c) -> - "DOP2("^(oper_display a)^","^(term_display b)^","^(term_display c)^")" - |DOPN(a,b) -> - "DOPN("^(oper_display a)^",[|"^(Array.fold_right (fun x i -> - (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|])" - |DOPL(a,b) -> - "DOPL("^(oper_display a)^",[|"^(List.fold_right (fun x i -> - (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|]" - |DLAM(a,b) -> "DLAM("^(name_display a)^","^(term_display b)^")" - |DLAMV(a,b) -> - "DLAMV("^(name_display a)^",[|"^(Array.fold_right (fun x i -> - (term_display x)^(if not(i="") then (";"^i) else "")) b "")^"|]" - |VAR(a) -> "VAR "^(string_of_id a) - |Rel(a) -> "Rel "^(string_of_int a) - and oper_display=function - Meta(a) -> "?"^(string_of_int a) -(* |XTRA(a,_) -> "XTRA("^a^",[ast])"*) - |Sort(a) -> "Sort("^(sort_display a)^")" -(* |Implicit -> "Implicit"*) - |Cast -> "Cast" - |Prod -> "Prod" - |Lambda -> "Lambda" - |AppL -> "AppL" - |Const(sp) -> "Const("^(string_of_path sp)^")" - |Abst(sp) -> "Abst("^(string_of_path sp)^")" - |MutInd(sp,i) -> "MutInd("^(string_of_path sp)^","^(string_of_int i)^")" - |MutConstruct((sp,i),j) -> - "MutConstruct(("^(string_of_path sp)^","^(string_of_int i)^"),"^ - (string_of_int j)^")" -(* |MutCase(ci) -> "MutCase("^(ci_display ci)^")"*) - |Fix(t,i) -> - "Fix([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="") - then (";"^i) else "")) t "")^"|],"^(string_of_int i)^")" - |CoFix(i) -> "CoFix "^(string_of_int i) - and sort_display=function - Prop(Pos) -> "Prop(Pos)" - |Prop(Null) -> "Prop(Null)" - |Type(_) -> "Type" -(* and ci_display=function - Some(sp,i) -> "Some("^(string_of_path sp)^","^(string_of_int i)^")" - |None -> "None"*) - and name_display=function - Name(id) -> "Name("^(string_of_id id)^")" - |Anonymous -> "Anonymous" - in - mSG [<'sTR (term_display csr);'fNL>] diff --git a/kernel/term.mli b/kernel/term.mli index 69db204fb0..ef75cde65d 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -561,5 +561,3 @@ val hcons_constr: (typed_type -> typed_type) val hcons1_constr : constr -> constr - -val constr_display: constr -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7737bdc6ce..1a45b8540b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1451,14 +1451,3 @@ let _ = if subtree_solved () then (rev_mutate top_of_tree; print_subgoals()) )) - -(*Only for debug*) -(*** -let _ = - add "PrintConstr" - (function - | [VARG_CONSTR c] -> - (fun () -> - Term.constr_display (constr_of_com empty_evd (initial_sign()) c)) - | _ -> bad_vernac_args "PrintConstr") -***) |