From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Tue, 19 Apr 2011 16:44:20 +0200 Subject: Imported Upstream version 8.3.pl2 --- pretyping/cases.ml | 4 ++-- pretyping/clenv.ml | 4 ++-- pretyping/evd.ml | 6 ++++-- pretyping/evd.mli | 4 ++-- pretyping/pretyping.ml | 7 +++++-- pretyping/tacred.ml | 9 ++++----- 6 files changed, 19 insertions(+), 15 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index bae89329..67bf7043 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 13728 2010-12-19 11:35:20Z herbelin $ *) +(* $Id: cases.ml 13962 2011-04-06 17:00:45Z herbelin $ *) open Util open Names @@ -1203,7 +1203,7 @@ and match_current pb tomatch = let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in let inst = List.map mkRel deps in { uj_val = applist (case, inst); - uj_type = substl inst typ } + uj_type = prod_applist typ inst } and compile_branch current names deps pb arsign eqn cstr = let sign, pb = build_branch current deps names pb arsign eqn cstr in diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index a41cdd6f..b9fd307c 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: clenv.ml 13902 2011-03-10 15:50:24Z msozeau $ *) open Pp open Util @@ -305,7 +305,7 @@ let evar_clenv_unique_resolver = clenv_unique_resolver let connect_clenv gls clenv = { clenv with - evd = evars_reset_evd gls.sigma clenv.evd; + evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd; env = Global.env_of_context gls.it.evar_hyps } (* [clenv_fchain mv clenv clenv'] diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 77442584..5d61e727 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evd.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: evd.ml 13902 2011-03-10 15:50:24Z msozeau $ *) open Pp open Util @@ -507,7 +507,9 @@ let empty = { metas=Metamap.empty } -let evars_reset_evd evd d = {d with evars = evd.evars} +let evars_reset_evd ?(with_conv_pbs=false) evd d = + {d with evars = evd.evars; + conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs} let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (EvarMap.find d.evars evk).evar_source diff --git a/pretyping/evd.mli b/pretyping/evd.mli index ce4e1b28..c68cfffe 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: evd.mli 13902 2011-03-10 15:50:24Z msozeau $ i*) (*i*) open Util @@ -177,7 +177,7 @@ val existential_opt_value : evar_map -> existential -> constr option val subst_evar_defs_light : substitution -> evar_map -> evar_map (* spiwack: this function seems to somewhat break the abstraction. *) -val evars_reset_evd : evar_map -> evar_map -> evar_map +val evars_reset_evd : ?with_conv_pbs:bool -> evar_map -> evar_map -> evar_map (* spiwack: [is_undefined_evar] should be considered a candidate diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1c17ff88..b8dc719b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 13408 2010-09-11 19:19:04Z herbelin $ *) +(* $Id: pretyping.ml 13780 2011-01-07 16:37:57Z herbelin $ *) open Pp open Util @@ -634,7 +634,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in let cj = match k with | VMcast when not (occur_existential cty || occur_existential tval) -> - ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj + (try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj + with Reduction.NotConvertible -> + error_actual_type_loc loc env !evdref cj tval) + | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval) in let v = mkCast (cj.uj_val, k, tval) in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 49ccb80c..68a67402 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: tacred.ml 13804 2011-01-27 00:41:34Z letouzey $ *) open Pp open Util @@ -216,8 +216,7 @@ let invert_name labs l na0 env sigma ref = function | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - let (mp,dp,_) = repr_con kn in - Some (EvalConst (make_con mp dp (label_of_id id))) in + Some (EvalConst (con_with_label kn (label_of_id id))) in match refi with | None -> None | Some ref -> @@ -481,7 +480,6 @@ let reduce_mind_case_use_function func env sigma mia = | CoFix (bodynum,(names,_,_) as cofix) -> let build_cofix_name = if isConst func then - let (mp,dp,_) = repr_con (destConst func) in let minargs = List.length mia.mcargs in fun i -> if i = bodynum then Some (minargs,func) @@ -492,7 +490,8 @@ let reduce_mind_case_use_function func env sigma mia = mutual inductive, try to reuse the global name if the block was indeed initially built as a global definition *) - let kn = make_con mp dp (label_of_id id) in + let kn = con_with_label (destConst func) (label_of_id id) + in try match constant_opt_value env kn with | None -> None (* TODO: check kn is correct *) -- cgit v1.2.3