diff options
Diffstat (limited to 'contrib/subtac/subtac_pretyping_F.ml')
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 45 |
1 files changed, 9 insertions, 36 deletions
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 65952750..46af5886 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping_F.ml 8889 2006-06-01 20:23:56Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 9316 2006-10-29 22:49:11Z herbelin $ *) open Pp open Util @@ -315,12 +315,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in let resj = match kind_of_term resj.uj_val with - | App (f,args) when isInd f -> + | App (f,args) when isInd f or isConst f -> let sigma = evars_of !isevars in - let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in - let s = snd (splay_arity env sigma t) in - on_judgment_type (set_inductive_level env s) resj - (* Rem: no need to send sigma: no head evar, it's an arity *) + let c = mkApp (f,Array.map (whd_evar sigma) args) in + let t = Retyping.get_type_of env sigma c in + make_judge c t | _ -> resj in inh_conv_coerce_to_tycon loc env isevars resj tycon @@ -557,35 +556,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env isevars lvar c).utj_val in nf_evar (evars_of !isevars) c' - (* [check_evars] fails if some unresolved evar remains *) - (* it assumes that the defined existentials have already been substituted - (should be done in unsafe_infer and unsafe_infer_type) *) - - let check_evars env initial_sigma isevars c = - let sigma = evars_of !isevars in - let rec proc_rec c = - match kind_of_term c with - | Evar (ev,args) -> - assert (Evd.mem sigma ev); - if not (Evd.mem initial_sigma ev) then - let (loc,k) = evar_source ev !isevars in - error_unsolvable_implicit loc env sigma k - | _ -> iter_constr proc_rec c - in - proc_rec c(*; - let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in - if pbs <> [] then begin - pperrnl - (str"TYPING OF "++Termops.print_constr_env env c++fnl()++ - prlist_with_sep fnl - (fun (pb,c1,c2) -> - Termops.print_constr c1 ++ - (if pb=Reduction.CUMUL then str " <="++ spc() - else str" =="++spc()) ++ - Termops.print_constr c2) - pbs ++ fnl()) - end*) - (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage retourne aussi le nouveau sigma... @@ -595,6 +565,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let isevars = ref (create_evar_defs sigma) in let j = pretype empty_tycon env isevars ([],[]) c in let j = j_nf_evar (evars_of !isevars) j in + let isevars,_ = consider_remaining_unif_problems env !isevars in check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j @@ -611,8 +582,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let isevars = ref (Evd.create_evar_defs sigma) in let c = pretype_gen isevars env lvar kind c in + let isevars,_ = consider_remaining_unif_problems env !isevars in + let c = nf_evar (evars_of isevars) c in if fail_evar then check_evars env sigma isevars c; - !isevars, c + isevars, c (** Entry points of the high-level type synthesis algorithm *) |