diff options
Diffstat (limited to 'contrib/xml')
| -rw-r--r-- | contrib/xml/cic2acic.ml | 6 | ||||
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 2 | ||||
| -rw-r--r-- | contrib/xml/proof2aproof.ml | 2 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 11 |
4 files changed, 11 insertions, 10 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index bac7ad7c..f217b037 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -64,7 +64,7 @@ let get_uri_of_var v pvars = in let rec search_in_open_sections = function - [] -> Util.error "Variable not found" + [] -> Util.error ("Variable "^v^" not found") | he::tl as modules -> let dirpath = N.make_dirpath modules in if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then @@ -167,10 +167,10 @@ let token_list_of_kernel_name tag = N.id_of_label (N.label kn), Lib.cwd () | Constant con -> N.id_of_label (N.con_label con), - Lib.library_part (LN.ConstRef con) + Lib.remove_section_part (LN.ConstRef con) | Inductive kn -> N.id_of_label (N.label kn), - Lib.library_part (LN.IndRef (kn,0)) + Lib.remove_section_part (LN.IndRef (kn,0)) in token_list_of_path dir id (etag_of_tag tag) ;; diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 518f6c11..a3336817 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -93,7 +93,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = let jty = execute env sigma ty None in let jty = assumption_of_judgment env sigma jty in let evar_context = - E.named_context_of_val (Evd.map sigma n).Evd.evar_hyps in + E.named_context_of_val (Evd.find sigma n).Evd.evar_hyps in let rec iter actual_args evar_context = match actual_args,evar_context with [],[] -> () diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index dff546c9..678b650c 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -47,7 +47,7 @@ let nf_evar sigma ~preserve = | _ -> T.mkApp (c', l') ) | _ -> T.mkApp (c', l')) - | T.Evar (e,l) when Evd.in_dom sigma e & Evd.is_defined sigma e -> + | T.Evar (e,l) when Evd.mem sigma e & Evd.is_defined sigma e -> aux (Evd.existential_value sigma (e,l)) | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l) | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 871a7f15..2235be4a 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -395,7 +395,7 @@ let mk_constant_obj id bo ty variables hyps = ty,params) ;; -let mk_inductive_obj sp packs variables nparams hyps finite = +let mk_inductive_obj sp mib packs variables nparams hyps finite = let module D = Declarations in let hyps = string_list_of_named_context_list hyps in let params = filter_params variables hyps in @@ -406,9 +406,9 @@ let mk_inductive_obj sp packs variables nparams hyps finite = (fun p i -> decr tyno ; let {D.mind_consnames=consnames ; - D.mind_typename=typename ; - D.mind_nf_arity=arity} = p + D.mind_typename=typename } = p in + let arity = Inductive.type_of_inductive (mib,p) in let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) @@ -524,11 +524,12 @@ let print internal glob_ref kind xml_library_root = G.lookup_constant kn in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Ln.IndRef (kn,_) -> + let mib = G.lookup_mind kn in let {D.mind_nparams=nparams; D.mind_packets=packs ; D.mind_hyps=hyps; - D.mind_finite=finite} = G.lookup_mind kn in - Cic2acic.Inductive kn,mk_inductive_obj kn packs variables nparams hyps finite + D.mind_finite=finite} = mib in + Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite | Ln.ConstructRef _ -> Util.anomaly ("print: this should not happen") in |