amelioration des messages d'erreurs vis a vis des evars

ajout automatique des chemins vers les sources au moment du Drop


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 10 insertions, 8 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 06a85319c3..70f4f70802 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -96,8 +96,8 @@ let unify_0 mc wc m n =
   let env = w_env wc
   and sigma = w_Underlying wc in
   let rec unirec_rec ((metasubst,evarsubst) as substn) m n =
-    let cM = whd_ise1 sigma m
-    and cN = whd_ise1 sigma n in 
+    let cM = Evarutil.whd_castappevar sigma m
+    and cN = Evarutil.whd_castappevar sigma n in 
     try 
       match (kind_of_term cM,kind_of_term cN) with
 	| IsCast (c,_), _ -> unirec_rec substn c cN
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 957605dfdd..f996086911 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -119,7 +119,7 @@ let w_Focusing sp wt =
 let w_Focus sp wc = ids_mod (extract_decl sp) wc
 
 let w_Underlying wc = (ts_it (ids_it wc)).decls
-let w_whd wc c      = whd_castappevar (w_Underlying wc) c
+let w_whd wc c      = Evarutil.whd_castappevar (w_Underlying wc) c
 let w_type_of wc c  = ctxt_type_of (ids_it wc) c
 let w_env     wc    = get_env (ids_it wc)
 let w_hyps    wc    = named_context (get_env (ids_it wc))
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 663b21a8a3..3f22a6f8ba 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -95,7 +95,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	if occur_meta conclty then
           raise (RefinerError (OccurMetaGoal conclty));
 	let ctxt = out_some goal.evar_info in 
-	(mk_goal ctxt hyps (nf_betaiota env sigma conclty))::goalacc, conclty
+	(mk_goal ctxt hyps (nf_betaiota conclty))::goalacc, conclty
 
     | IsCast (t,ty) ->
 	let _ = type_of env sigma ty in
@@ -135,7 +135,7 @@ and mk_hdgoals sigma goal goalacc trm =
     | IsCast (c,ty) when isMeta c ->
 	let _ = type_of env sigma ty in
 	let ctxt = out_some goal.evar_info in  
-	(mk_goal ctxt hyps (nf_betaiota env sigma ty))::goalacc,ty
+	(mk_goal ctxt hyps (nf_betaiota ty))::goalacc,ty
 
     | IsApp (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
@@ -168,10 +168,12 @@ and mk_casegoals sigma goal goalacc p c =
   let env = evar_env goal in
   let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
+  let pj = {uj_val=p; uj_type=pt} in 
   let indspec =
     try find_rectype env sigma ct
     with Induc -> anomaly "mk_casegoals" in
-  let (lbrty,conclty,_) = type_case_branches env sigma indspec pt p c in
+  let (lbrty,conclty,_) =
+    type_case_branches env sigma indspec pj c in
   (acc'',lbrty,conclty)
 
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 8e358adea2..cfb5e64f92 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -49,7 +49,7 @@ let rec and_status = function
    (i.e. when the sigma of the proof tree changes) *)
 
 let norm_goal sigma gl =
-  let red_fun = nf_ise1 sigma in
+  let red_fun = Evarutil.nf_evar sigma in
   let ncl = red_fun gl.evar_concl in
   { evar_concl = ncl;
     evar_hyps = map_named_context red_fun gl.evar_hyps;
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b3ad1225e5..b68196ff3b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -98,7 +98,7 @@ let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_red_product               = pf_reduce red_product
 let pf_nf                        = pf_reduce nf
-let pf_nf_betaiota               = pf_reduce nf_betaiota
+let pf_nf_betaiota               = pf_reduce (fun _ _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 let pf_type_of                   = pf_reduce type_of