diff options
Diffstat (limited to 'plugins/xml/cic2acic.ml')
| -rw-r--r-- | plugins/xml/cic2acic.ml | 16 |
1 files changed, 8 insertions, 8 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'' ; |