aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml')
-rw-r--r--plugins/xml/cic2acic.ml16
-rw-r--r--plugins/xml/doubleTypeInference.ml17
-rw-r--r--plugins/xml/xmlcommand.ml13
3 files changed, 23 insertions, 23 deletions
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index bf46065d0..bbaef1e70 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -190,6 +190,7 @@ module CPropRetyping =
let typeur sigma metamap =
let rec type_of env cstr=
match Term.kind_of_term cstr with
+ | T.Proj _ -> assert false
| T.Meta n ->
(try T.strip_outer_cast (Int.List.assoc n metamap)
with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
@@ -202,9 +203,7 @@ let typeur sigma metamap =
ty
with Not_found ->
Errors.anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound"))
- | T.Const c ->
- let cb = Environ.lookup_constant c env in
- Typeops.type_of_constant_type env (cb.Declarations.const_type)
+ | T.Const c -> Typeops.type_of_constant_in env c
| T.Evar ev -> Evd.existential_type sigma ev
| T.Ind ind -> Inductiveops.type_of_inductive env ind
| T.Construct cstr -> Inductiveops.type_of_constructor env cstr
@@ -355,7 +354,7 @@ Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the doub
{DoubleTypeInference.synthesized =
Reductionops.nf_beta evar_map
(CPropRetyping.get_type_of env evar_map
- (Termops.refresh_universes tt)) ;
+ ((* Termops.refresh_universes *) tt)) ;
DoubleTypeInference.expected = None}
in
let innersort =
@@ -484,7 +483,8 @@ print_endline "PASSATO" ; flush stdout ;
(* Now that we have all the auxiliary functions we *)
(* can finally proceed with the main case analysis. *)
match Term.kind_of_term tt with
- Term.Rel n ->
+ | Term.Proj _ -> assert false
+ | Term.Rel n ->
let id =
match List.nth (Environ.rel_context env) (n - 1) with
(Names.Name id,_,_) -> id
@@ -670,7 +670,7 @@ print_endline "PASSATO" ; flush stdout ;
explicit_substitute_and_eta_expand_if_required h
(Array.to_list t) t'
compute_result_if_eta_expansion_not_required
- | Term.Const kn ->
+ | Term.Const (kn,u) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if is_a_Prop innersort && expected_available then
add_inner_type fresh_id'' ;
@@ -681,7 +681,7 @@ print_endline "PASSATO" ; flush stdout ;
explicit_substitute_and_eta_expand_if_required tt []
(List.map snd subst')
compute_result_if_eta_expansion_not_required
- | Term.Ind (kn,i) ->
+ | Term.Ind ((kn,i),u) ->
let compute_result_if_eta_expansion_not_required _ _ =
Acic.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i)
in
@@ -689,7 +689,7 @@ print_endline "PASSATO" ; flush stdout ;
explicit_substitute_and_eta_expand_if_required tt []
(List.map snd subst')
compute_result_if_eta_expansion_not_required
- | Term.Construct ((kn,i),j) ->
+ | Term.Construct (((kn,i),j),u) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if is_a_Prop innersort && expected_available then
add_inner_type fresh_id'' ;
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index d54308165..c8717e008 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -64,7 +64,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
T.Meta n ->
Errors.error
"DoubleTypeInference.double_type_of: found a non-instanciated goal"
-
+ | T.Proj _ -> assert false
| T.Evar ((n,l) as ev) ->
let ty = Unshare.unshare (Evd.existential_type sigma ev) in
let jty = execute env sigma ty None in
@@ -99,7 +99,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
Typeops.judge_of_variable env id
| T.Const c ->
- E.make_judge cstr (Typeops.type_of_constant env c)
+ E.make_judge cstr (fst (Typeops.type_of_constant env c))
| T.Ind ind ->
E.make_judge cstr (Inductiveops.type_of_inductive env ind)
@@ -112,15 +112,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma c) in
let cj = execute env sigma c (Some expectedtype) in
let pj = execute env sigma p None in
- let (expectedtypes,_,_) =
+ let (expectedtypes,_) =
let indspec = Inductive.find_rectype env cj.Environ.uj_type in
Inductive.type_case_branches env indspec pj cj.Environ.uj_val
in
let lfj =
execute_array env sigma lf
(Array.map (function x -> Some x) expectedtypes) in
- let (j,_) = Typeops.judge_of_case env ci pj cj lfj in
- j
+ Typeops.judge_of_case env ci pj cj lfj
| T.Fix ((vn,i as vni),recdef) ->
let (_,tys,_ as recdef') = execute_recdef env sigma recdef in
@@ -141,10 +140,10 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
(*CSC: again once Judicael will introduce his non-bugged algebraic *)
(*CSC: universes. *)
(try
- Typeops.judge_of_type u
+ (*FIXME*) (Typeops.judge_of_type u)
with _ -> (* Successor of a non universe-variable universe anomaly *)
Pp.msg_warning (Pp.str "Universe refresh performed!!!");
- Typeops.judge_of_type (Termops.new_univ ())
+ (*FIXME*) (Typeops.judge_of_type (Universes.new_univ Names.empty_dirpath))
)
| T.App (f,args) ->
@@ -165,7 +164,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
Array.of_list (aux j.Environ.uj_type (Array.to_list args))
in
let jl = execute_array env sigma args expected_args in
- let (j,_) = Typeops.judge_of_apply env j jl in
+ let j = Typeops.judge_of_apply env j jl in
j
| T.Lambda (name,c1,c2) ->
@@ -212,7 +211,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in
let tj = execute env sigma t None in
let tj = type_judgment env sigma tj in
- let j, _ = Typeops.judge_of_cast env cj k tj in
+ let j = Typeops.judge_of_cast env cj k tj in
j
in
let synthesized = E.j_type judgement in
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 5f26e2bac..3d655920b 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -175,16 +175,17 @@ let find_hyps t =
| Term.Meta _
| Term.Evar _
| Term.Sort _ -> l
+ | Term.Proj _ -> ignore(Errors.todo "Proj in find_hyps"); assert false
| Term.Cast (te,_, ty) -> aux (aux l te) ty
| Term.Prod (_,s,t) -> aux (aux l s) t
| Term.Lambda (_,s,t) -> aux (aux l s) t
| Term.LetIn (_,s,_,t) -> aux (aux l s) t
| Term.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl
- | Term.Const con ->
+ | Term.Const (con, _) ->
let hyps = (Global.lookup_constant con).Declarations.const_hyps in
map_and_filter l hyps @ l
- | Term.Ind ind
- | Term.Construct (ind,_) ->
+ | Term.Ind (ind,_)
+ | Term.Construct ((ind,_),_) ->
let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in
map_and_filter l hyps @ l
| Term.Case (_,t1,t2,b) ->
@@ -243,8 +244,8 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
let {Declarations.mind_consnames=consnames ;
Declarations.mind_typename=typename } = p
in
- let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in
- let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in
+ let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),Univ.Instance.empty)(*FIXME*) in
+ let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),Univ.Instance.empty)(*FIXME*) in
let cons =
(Array.fold_right (fun (name,lc) i -> (name,lc)::i)
(Array.mapi
@@ -379,7 +380,7 @@ let print internal glob_ref kind xml_library_root =
let val0 = Declareops.body_of_constant cb in
let typ = cb.Declarations.const_type in
let hyps = cb.Declarations.const_hyps in
- let typ = Typeops.type_of_constant_type (Global.env()) typ in
+ let typ = (* Typeops.type_of_constant_type (Global.env()) *) typ in
Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
| Globnames.IndRef (kn,_) ->
let mib = Global.lookup_mind kn in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 10:08:55 +0000