correction de bugs:

- subst_term_gen ne depliait pas les constantes locales de maniere uniforme
- la tactique Simpl ne simplifiait pas les constantes definies dans le
  contexte de but
- la conversion d'un constr vers identificateur ne prenait pas en compte
  les inductifs et constructeurs


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

3 files changed, 90 insertions, 45 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f2c185621..95acf3a6c 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -367,7 +367,7 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
   let subbodies = list_tabulate make_Fi nbodies in
   substl subbodies bodies.(bodynum)
 
-let reduce_mind_case_use_function kn env mia =
+let reduce_mind_case_use_function func env mia =
   match kind_of_term mia.mconstr with 
     | Construct(ind_sp,i as cstr_sp) ->
 	let real_cargs = snd (list_chop mia.mci.ci_npar mia.mcargs) in
@@ -376,37 +376,39 @@ let reduce_mind_case_use_function kn env mia =
 	let build_fix_name i =
 	  match names.(i) with 
 	    | Name id ->
-		let (mp,dp,_) = repr_kn kn in
-		let kn = make_kn mp dp (label_of_id id) in
-		(match constant_opt_value env kn with
-		  | None -> None
-		  | Some _ -> Some (mkConst kn))
+                if isConst func then
+		  let (mp,dp,_) = repr_kn (destConst func) in
+		  let kn = make_kn mp dp (label_of_id id) in
+		  (match constant_opt_value env kn with
+		    | None -> None
+		    | Some _ -> Some (mkConst kn))
+                else None
 	    | Anonymous -> None in 
 	let cofix_def = contract_cofix_use_function build_fix_name cofix in
 	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
-let special_red_case env whfun (ci, p, c, lf)  =
+let special_red_case sigma env whfun (ci, p, c, lf)  =
   let rec redrec s = 
     let (constr, cargs) = whfun s in 
-    match kind_of_term constr with 
-      | Const cst -> 
-          (if not (is_evaluable env (EvalConstRef cst)) then
-            raise Redelimination;
-	  let gvalue = constant_value env cst in
-	  if reducible_mind_case gvalue then
-	    reduce_mind_case_use_function cst env
-	      {mP=p; mconstr=gvalue; mcargs=list_of_stack cargs;
-               mci=ci; mlf=lf}
-	  else
-	    redrec (gvalue, cargs))
-      | _ ->
-          if reducible_mind_case constr then
-            reduce_mind_case
-	      {mP=p; mconstr=constr; mcargs=list_of_stack cargs;
-	       mci=ci; mlf=lf}
-          else 
-	    raise Redelimination
+    if isEvalRef env constr then
+      let ref = destEvalRef constr in
+      match reference_opt_value sigma env ref with
+        | None -> raise Redelimination
+        | Some gvalue ->
+	    if reducible_mind_case gvalue then
+	      reduce_mind_case_use_function constr env
+	        {mP=p; mconstr=gvalue; mcargs=list_of_stack cargs;
+                mci=ci; mlf=lf}
+	    else
+	      redrec (gvalue, cargs)
+    else
+      if reducible_mind_case constr then
+        reduce_mind_case
+	  {mP=p; mconstr=constr; mcargs=list_of_stack cargs;
+	  mci=ci; mlf=lf}
+      else 
+	raise Redelimination
   in 
   redrec (c, empty_stack)
 
@@ -416,7 +418,7 @@ let rec red_elim_const env sigma ref largs =
     | EliminationCases n when stack_args_size largs >= n ->
 	let c = reference_value sigma env ref in
 	let c', lrest = whd_betadeltaeta_state env sigma (c,largs) in
-        (special_red_case env (construct_const env sigma) (destCase c'),
+        (special_red_case sigma env (construct_const env sigma) (destCase c'),
 	 lrest)
     | EliminationFix (min,infos) when stack_args_size largs >=min ->
 	let c = reference_value sigma env ref in
@@ -457,7 +459,7 @@ and construct_const env sigma =
       | LetIn (n,b,t,c) -> stacklam hnfstack [b] c stack
       | Case (ci,p,c,lf) ->
           hnfstack 
-	    (special_red_case env
+	    (special_red_case sigma env
               (construct_const env sigma) (ci,p,c,lf), stack)
       | Construct _ -> s
       | CoFix _ -> s
@@ -535,7 +537,7 @@ let hnf_constr env sigma c =
       | Case (ci,p,c,lf) ->
           (try
              redrec 
-	       (special_red_case env (whd_betadeltaiota_state env sigma) 
+	       (special_red_case sigma env (whd_betadeltaiota_state env sigma) 
 		  (ci, p, c, lf), largs)
            with Redelimination -> 
 	     app_stack s)
@@ -575,7 +577,7 @@ let whd_nf env sigma c =
       | Cast (c,_) -> nf_app (c, stack)
       | Case (ci,p,d,lf) ->
           (try
-             nf_app (special_red_case env nf_app (ci,p,d,lf), stack)
+             nf_app (special_red_case sigma env nf_app (ci,p,d,lf), stack)
            with Redelimination -> 
 	     s)
       | Fix fix ->
@@ -825,7 +827,7 @@ let one_step_reduce env sigma c =
       | LetIn (_,f,_,cl) -> (subst1 f cl,largs)
       | Case (ci,p,c,lf) ->
           (try
-	     (special_red_case env (whd_betadeltaiota_state env sigma)
+	     (special_red_case sigma env (whd_betadeltaiota_state env sigma)
 	       (ci,p,c,lf), largs)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9fc7dc976..442eb7a5d 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -236,24 +236,55 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
       mkCoFix (ln,(lna,tl',bl'))
 
 (* strong *)
-let map_constr_with_full_binders g f l c = match kind_of_term c with
+let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
-  | Cast (c,t) -> mkCast (f l c, f l t)
-  | Prod (na,t,c) -> mkProd (na, f l t, f (g (na,None,t) l) c)
-  | Lambda (na,t,c) -> mkLambda (na, f l t, f (g (na,None,t) l) c)
-  | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g (na,Some b,t) l) c)
-  | App (c,al) -> mkApp (f l c, Array.map (f l) al)
-  | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
-  | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
+    | Construct _) -> cstr
+  | Cast (c,t) -> 
+      let c' = f l c in
+      let t' = f l t in
+      if c==c' && t==t' then cstr else mkCast (c', t')
+  | Prod (na,t,c) ->
+      let t' = f l t in
+      let c' = f (g (na,None,t) l) c in
+      if t==t' && c==c' then cstr else mkProd (na, t', c')
+  | Lambda (na,t,c) ->
+      let t' = f l t in
+      let c' = f (g (na,None,t) l) c in
+      if t==t' && c==c' then cstr else  mkLambda (na, t', c')
+  | LetIn (na,b,t,c) ->
+      let b' = f l b in
+      let t' = f l t in
+      let c' = f (g (na,Some b,t) l) c in
+      if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
+  | App (c,al) ->
+      let c' = f l c in
+      let al' = Array.map (f l) al in
+      if c==c' && array_for_all2 (==) al al' then cstr else mkApp (c', al')
+  | Evar (e,al) ->
+      let al' = Array.map (f l) al in
+      if array_for_all2 (==) al al' then cstr else mkEvar (e, al')
+  | Case (ci,p,c,bl) ->
+      let p' = f l p in
+      let c' = f l c in
+      let bl' = Array.map (f l) bl in
+      if p==p' && c==c' && array_for_all2 (==) bl bl' then cstr else
+        mkCase (ci, p', c', bl')
   | Fix (ln,(lna,tl,bl)) ->
+      let tl' = Array.map (f l) tl in
       let l' =
         array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
-      mkFix (ln,(lna,Array.map (f l) tl, Array.map (f l') bl))
+      let bl' = Array.map (f l') bl in
+      if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
+      then cstr
+      else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
+      let tl' = Array.map (f l) tl in
       let l' =
         array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
-      mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+      let bl' = Array.map (f l') bl in
+      if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
+      then cstr
+      else mkCoFix (ln,(lna,tl',bl'))
 
 
 (* Equality modulo let reduction *)
@@ -416,10 +447,13 @@ let subst_term_gen eq_fun env c t =
       | Some x -> x
       | None ->
     (if eq_fun e c t then mkRel k
-     else
-       map_constr_with_full_binders
-         (fun d (e,k,c) -> (push_rel d e,k+1,lift 1 c))
-         substrec kc t)
+    else
+      let red_t = whd_locals env t in
+      let red_t' =
+        map_constr_with_full_binders
+          (fun d (e,k,c) -> (push_rel d e,k+1,lift 1 c))
+          substrec kc red_t in
+      if red_t == red_t' then t else red_t')
   in 
   substrec (env,1,nf_locals env c) t
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 55134310f..3c50c2672 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -868,6 +868,15 @@ VIdentifier id
 (* Gives the identifier corresponding to an Identifier tactic_arg *)
 let id_of_Identifier = function
   | VConstr c when isVar c -> destVar c
+  | VConstr c ->
+      (match kind_of_term c with
+          Var id -> id
+        | Const sp -> id_of_global None (ConstRef sp)
+        | Ind sp -> id_of_global None (IndRef sp)
+        | Construct sp -> id_of_global None (ConstructRef sp)
+        | _ ->
+            anomalylabstrm "id_of_Identifier"
+              (str "Not an IDENTIFIER tactic_arg"))
   | VIdentifier id -> id
   | _ ->
     anomalylabstrm "id_of_Identifier" (str "Not an IDENTIFIER tactic_arg")