Changement des named_context

Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs


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

12 files changed, 72 insertions, 58 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index dd07c2b90..e6d1194a5 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -189,7 +189,7 @@ let make_exact_entry name (c,cty) =
 	   { hname=name; pri=0; pat=None; code=Give_exact c })
 
 let dummy_goal =
-  {it={evar_hyps=empty_named_context;evar_concl=mkProp;evar_body=Evar_empty};
+  {it={evar_hyps=empty_named_context_val;evar_concl=mkProp;evar_body=Evar_empty};
    sigma=Evd.empty}
 
 let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index b79e6c608..6cf0cc981 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -89,7 +89,7 @@ let autorewrite_in id tac_main lbas gl =
   let to_be_cleared = ref false in
    fun dir cstr gl ->
     let last_hyp_id =
-     match gl.Evd.it.Evd.evar_hyps with
+     match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) with
         (last_hyp_id,_,_)::_ -> last_hyp_id
       | _ -> (* even the hypothesis id is missing *)
              error ("No such hypothesis : " ^ (string_of_id !id))
@@ -98,7 +98,7 @@ let autorewrite_in id tac_main lbas gl =
     let gls = (fst gl').Evd.it in
     match gls with
        g::_ ->
-        (match g.Evd.evar_hyps with
+        (match Environ.named_context_of_val g.Evd.evar_hyps with
             (lastid,_,_)::_ ->
               if last_hyp_id <> lastid then
                begin
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 52f5f011a..e3cb25632 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -85,7 +85,8 @@ let e_constructor_tac boundopt i lbind gl =
   end;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
   let apply_tac = e_resolve_with_bindings_tac (cons,lbind) in
-  (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl
+  (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast
+; intros; apply_tac]) gl
 
 let e_one_constructor i = e_constructor_tac None i
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 57d9ab58a..23e4d311c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -690,7 +690,7 @@ let try_delta_expand env sigma t =
     match kind_of_term c with
       | Construct _ -> whdt
       | App (f,_)  -> hd_rec f
-      | Cast (c,_) -> hd_rec c
+      | Cast (c,_,_) -> hd_rec c
       | _  -> t
   in 
   hd_rec whdt 
@@ -1036,7 +1036,7 @@ let unfold_body x gl =
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
     [tclMAP (fun h -> reduct_in_hyp rfun h) hl;
-     reduct_in_concl rfun] gl
+     reduct_in_concl (rfun,DEFAULTcast)] gl
 
 
 
@@ -1088,8 +1088,9 @@ let subst_one x gl =
   let introtac = function
       (id,None,_) -> intro_using id
     | (id,Some hval,htyp) ->
-        forward true (Name id) (mkCast(replace_term varx rhs hval,
-                                       replace_term varx rhs htyp)) in
+        forward true (Name id) (mkCast(replace_term varx rhs hval,DEFAULTcast,
+                                       replace_term varx rhs htyp))
+  in
   let need_rewrite = dephyps <> [] || depconcl in
   tclTHENLIST 
     ((if need_rewrite then
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index a0be2149a..d1a2b40b1 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -34,7 +34,7 @@ let instantiate n rawc ido gl =
     match ido with
 	ConclLocation () -> evar_list sigma gl.it.evar_concl 
       | HypLocation (id,hloc) ->
-	  let decl = lookup_named id gl.it.evar_hyps in
+	  let decl = Environ.lookup_named_val id gl.it.evar_hyps in
 	    match hloc with
 		InHyp ->  
 		  (match decl with 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 60d05ec70..481b78683 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -216,7 +216,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     errorlabstrm "lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature");
   *)
-  let invSign = named_context invEnv in
+  let invSign = named_context_val invEnv in
   let pfs = mk_pftreestate (mk_goal invSign invGoal) in
   let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in
   let (pfterm,meta_types) = extract_open_pftreestate pfs in
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 493232d3c..a6b904c05 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -97,9 +97,9 @@ let replace_by_meta env = function
       (* quand on introduit une mv on calcule son type *)
       let ty = match kind_of_term c with
 	| Lambda (Name id,c1,c2) when isCast c2 ->
-	    mkNamedProd id c1 (snd (destCast c2))
+	    let _,_,t = destCast c2 in mkNamedProd id c1 t
 	| Lambda (Anonymous,c1,c2) when isCast c2 ->
-	    mkArrow c1 (snd (destCast c2))
+	    let _,_,t = destCast c2 in mkArrow c1 t
 	| _ -> (* (App _ | Case _) -> *)
 	    Retyping.get_type_of_with_meta env Evd.empty mm c
 	(*
@@ -108,7 +108,7 @@ let replace_by_meta env = function
 	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" 
         *)
       in
-      mkCast (m,ty),[n,ty],[Some th]
+      mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]
 
 exception NoMeta
 
@@ -138,9 +138,10 @@ let rec compute_metamap env c = match kind_of_term c with
   | Meta n ->
       TH (c,[],[None])
 
-  | Cast (m,ty) when isMeta m -> 
+  | Cast (m,_, ty) when isMeta m -> 
       TH (c,[destMeta m,ty],[None])
 
+
   (* abstraction => il faut décomposer si le terme dessous n'est pas pur
    *    attention : dans ce cas il faut remplacer (Rel 1) par (Var x)
    *    où x est une variable FRAICHE *)
@@ -216,7 +217,7 @@ let rec compute_metamap env c = match kind_of_term c with
       end
 	      
   (* Cast. Est-ce bien exact ? *)
-  | Cast (c,t) -> compute_metamap env c
+  | Cast (c,_,t) -> compute_metamap env c
       (*let TH (c',mm,sgp) = compute_metamap sign c in
 	TH (mkCast (c',t),mm,sgp) *)
       
@@ -258,7 +259,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
     | Meta _ , _ ->
 	tclIDTAC gl
 
-    | Cast (c,_), _ when isMeta c ->
+    | Cast (c,_,_), _ when isMeta c ->
 	tclIDTAC gl
 	  
     (* terme pur => refine *)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 5cd163364..316f3c276 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1464,7 +1464,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
               | (he::tl) as a->
                  let typnf = Reduction.whd_betadeltaiota env typ in
                   match kind_of_term typnf with
-                    Cast (typ,_) ->
+                    Cast (typ,_,_) ->
                      find_non_dependent_function env c c_args_rev typ
                       f_args_rev a_rev a
                   | Prod (name,s,t) ->
@@ -1676,7 +1676,7 @@ let syntactic_but_representation_of_marked_but hole_relation hole_direction =
        else
         let c_is_proper =
          let typ = mkApp (rel_out, [| c ; c |]) in
-          mkCast (Evarutil.mk_new_meta (),typ)
+          mkCast (Evarutil.mk_new_meta (),DEFAULTcast, typ)
         in
          mkApp ((Lazy.force coq_ProperElementToKeep),
           [| hole_relation ; hole_direction; precise_out ;
@@ -1759,7 +1759,8 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
      let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in
       let th' = mkApp (proj, [|impl2; impl1; th|]) in
        Tactics.refine
-        (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl in
+        (mkApp (th',[|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|]))
+	gl in
    let if_output_relation_is_if gl =
     let th =
      apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
@@ -1767,15 +1768,15 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
     in
      let new_but = Termops.replace_term c1 c2 but in
       Tactics.refine
-       (mkApp (th, [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl
-   in
-    if output_relation = (Lazy.force coq_iff_relation) then
+       (mkApp (th, [|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|]))
+       gl in
+   if output_relation = (Lazy.force coq_iff_relation) then
      if_output_relation_is_iff gl
-    else
+   else
      if_output_relation_is_if gl
   with
-   Optimize ->
-    !general_rewrite (input_direction = Left2Right) (snd hyp) gl
+    Optimize ->
+      !general_rewrite (input_direction = Left2Right) (snd hyp) gl
 
 let analyse_hypothesis gl c =
  let ctype = pf_type_of gl c in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5948da2b8..177c3ffd8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1191,7 +1191,9 @@ open Evd
 let solvable_by_tactic env evi (ev,args) src = 
   match (!implicit_tactic, src) with
   | Some tac, (ImplicitArg _ | QuestionMark)
-      when evi.evar_hyps = Environ.named_context env ->
+      when 
+	Environ.named_context_of_val evi.evar_hyps = 
+	Environ.named_context env ->
       let id = id_of_string "H" in
       start_proof id IsLocal evi.evar_hyps evi.evar_concl (fun _ _ -> ());
       begin
@@ -1510,7 +1512,7 @@ and interp_letin ist gl = function
       with Not_found ->
       try
 	let t = tactic_of_value v in
-	let ndc = Environ.named_context env in
+	let ndc = Environ.named_context_val env in
 	start_proof id IsLocal ndc typ (fun _ _ -> ());
 	by t;
 	let (_,({const_entry_body = pft},_,_)) = cook_proof () in
@@ -1520,7 +1522,7 @@ and interp_letin ist gl = function
 	delete_proof (dummy_loc,id);
 	errorlabstrm "Tacinterp.interp_letin"
           (str "Term or fully applied tactic expected in Let")
-    in (id,VConstr (mkCast (csr,typ)))::(interp_letin ist gl tl)
+    in (id,VConstr (mkCast (csr,DEFAULTcast, typ)))::(interp_letin ist gl tl)
 
 (* Interprets the Match Context expressions *)
 and interp_match_context ist g lz lr lmr =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5079a1010..d1a7507c7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -50,7 +50,7 @@ let rec nb_prod x =
     match kind_of_term c with
         Prod(_,_,t) -> count (n+1) t
       | LetIn(_,a,_,t) -> count n (subst1 a t)
-      | Cast(c,_) -> count n c
+      | Cast(c,_,_) -> count n c
       | _ -> n
   in count 0 x
 
@@ -144,8 +144,8 @@ type tactic_reduction = env -> evar_map -> constr -> constr
    reduction function either to the conclusion or to a 
    certain hypothesis *)
 
-let reduct_in_concl redfun gl = 
-  convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) gl
+let reduct_in_concl (redfun,sty) gl = 
+  convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
 
 let reduct_in_hyp redfun (id,_,(where,where')) gl =
   let (_,c, ty) = pf_get_hyp gl id in
@@ -165,7 +165,7 @@ let reduct_in_hyp redfun (id,_,(where,where')) gl =
       convert_hyp_no_check (id,Some b',ty') gl
 
 let reduct_option redfun = function
-  | Some id -> reduct_in_hyp   redfun id 
+  | Some id -> reduct_in_hyp   (fst redfun) id 
   | None    -> reduct_in_concl redfun 
 
 (* The following tactic determines whether the reduction
@@ -188,7 +188,8 @@ let change_on_subterm cv_pb t = function
   | Some occl -> contextually false occl (change_and_check Reduction.CONV t) 
 
 let change_in_concl occl t =
-  reduct_in_concl (change_on_subterm Reduction.CUMUL t occl) 
+  reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
+
 let change_in_hyp occl t   =
   reduct_in_hyp (change_on_subterm Reduction.CONV t occl)
 
@@ -205,22 +206,23 @@ let change occl c cls =
   onClauses (change_option occl c) cls
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
-let red_in_concl        = reduct_in_concl red_product
+let red_in_concl        = reduct_in_concl (red_product,DEFAULTcast)
 let red_in_hyp          = reduct_in_hyp   red_product
-let red_option          = reduct_option   red_product
-let hnf_in_concl        = reduct_in_concl hnf_constr
+let red_option          = reduct_option   (red_product,DEFAULTcast)
+let hnf_in_concl        = reduct_in_concl (hnf_constr,DEFAULTcast)
 let hnf_in_hyp          = reduct_in_hyp   hnf_constr
-let hnf_option          = reduct_option   hnf_constr
-let simpl_in_concl      = reduct_in_concl nf
+let hnf_option          = reduct_option   (hnf_constr,DEFAULTcast)
+let simpl_in_concl      = reduct_in_concl (nf,DEFAULTcast)
 let simpl_in_hyp        = reduct_in_hyp   nf
-let simpl_option        = reduct_option   nf
-let normalise_in_concl  = reduct_in_concl compute
+let simpl_option        = reduct_option   (nf,DEFAULTcast)
+let normalise_in_concl  = reduct_in_concl (compute,DEFAULTcast)
 let normalise_in_hyp    = reduct_in_hyp   compute
-let normalise_option    = reduct_option   compute
-let unfold_in_concl loccname   = reduct_in_concl (unfoldn loccname) 
-let unfold_in_hyp   loccname   = reduct_in_hyp   (unfoldn loccname) 
-let unfold_option   loccname   = reduct_option   (unfoldn loccname) 
-let pattern_option l = reduct_option (pattern_occs l)
+let normalise_option    = reduct_option   (compute,DEFAULTcast)
+let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
+let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,DEFAULTcast)
+let unfold_in_hyp   loccname = reduct_in_hyp   (unfoldn loccname) 
+let unfold_option   loccname = reduct_option (unfoldn loccname,DEFAULTcast) 
+let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast)
 
 (* A function which reduces accordingly to a reduction expression,
    as the command Eval does. *)
@@ -346,7 +348,9 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl =
   let rec aux ccl =
     match pf_lookup_hypothesis_as_renamed env ccl h with
       | None when red ->
-          aux (Redexpr.reduction_of_red_expr (Red true) env (project gl) ccl)
+          aux 
+	    ((fst (Redexpr.reduction_of_red_expr (Red true))) 
+	       env (project gl) ccl)
       | x -> x
   in
   try aux (pf_concl gl)
@@ -433,7 +437,7 @@ let rec intros_rmove = function
  *  of the type of a term. *)
 
 let apply_type hdcty argl gl =
-  refine (applist (mkCast (Evarutil.mk_new_meta(),hdcty),argl)) gl
+  refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl
     
 let apply_term hdc argl gl =
   refine (applist (hdc,argl)) gl
@@ -443,7 +447,7 @@ let bring_hyps hyps =
   else
     (fun gl ->
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
-      let f = mkCast (Evarutil.mk_new_meta(),newcl) in
+      let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in
       refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
 
 (* Resolution with missing arguments *)
@@ -749,7 +753,7 @@ let letin_tac with_eq name c occs gl =
   let t = refresh_universes (pf_type_of gl c) in
   let newcl = mkNamedLetIn id c t ccl in
   tclTHENLIST
-    [ convert_concl_no_check newcl;
+    [ convert_concl_no_check newcl DEFAULTcast;
       intro_gen (IntroMustBe id) lastlhyp true;
       if with_eq then tclIDTAC else thin_body [id];
       tclMAP convert_hyp_no_check depdecls ] gl
@@ -882,7 +886,8 @@ let constructor_tac boundopt i lbind gl =
   end;
   let cons = mkConstruct (ith_constructor_of_inductive mind i) in
   let apply_tac = apply_with_bindings (cons,lbind) in
-  (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl
+  (tclTHENLIST 
+     [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
 
 let one_constructor i = constructor_tac None i
 
@@ -1391,7 +1396,8 @@ let induction_tac varname typ ((elimc,lbindelimc),elimt) gl =
   let c = mkVar varname in
   let indclause  = make_clenv_binding gl (c,typ) NoBindings  in
   let elimclause =
-    make_clenv_binding gl (mkCast (elimc,elimt),elimt) lbindelimc in
+    make_clenv_binding gl 
+      (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
   elimination_clause_scheme true elimclause indclause gl
 
 let make_up_names7 n ind (old_style,cname) = 
@@ -1900,9 +1906,9 @@ let abstract_subproof name tac gls =
       (fun (id,_,_ as d) (s1,s2) -> 
 	 if mem_named_context id current_sign &
            interpretable_as_section_decl (Sign.lookup_named id current_sign) d
-         then (s1,add_named_decl d s2)
+         then (s1,push_named_context_val d s2)
 	 else (add_named_decl d s1,s2)) 
-      global_sign (empty_named_context,empty_named_context) in
+      global_sign (empty_named_context,empty_named_context_val) in
   let na = next_global_ident_away false name (pf_ids_of_hyps gls) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
   if occur_existential concl then
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 5b03a79dd..f3da4a8c9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -46,7 +46,7 @@ exception Bound
 
 val introduction    : identifier -> tactic
 val refine          : constr -> tactic
-val convert_concl   : constr -> tactic
+val convert_concl   : constr -> cast_kind -> tactic
 val convert_hyp     : named_declaration -> tactic
 val thin            : identifier list -> tactic
 val mutual_fix      :
@@ -110,8 +110,8 @@ val exact_proof      : Topconstr.constr_expr -> tactic
 type tactic_reduction = env -> evar_map -> constr -> constr
 
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
-val reduct_option     : tactic_reduction -> simple_clause -> tactic
-val reduct_in_concl   : tactic_reduction -> tactic
+val reduct_option     : tactic_reduction * cast_kind -> simple_clause -> tactic
+val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
 val change_in_concl   : constr occurrences option -> constr -> tactic
 val change_in_hyp     : constr occurrences option -> constr -> hyp_location ->
   tactic
@@ -124,9 +124,10 @@ val hnf_option        : simple_clause -> tactic
 val simpl_in_concl    : tactic
 val simpl_in_hyp      : hyp_location        -> tactic
 val simpl_option      : simple_clause -> tactic
-val normalise_in_concl: tactic
+val normalise_in_concl : tactic
 val normalise_in_hyp  : hyp_location        -> tactic
 val normalise_option  : simple_clause -> tactic
+val normalise_vm_in_concl : tactic
 val unfold_in_concl   : (int list * evaluable_global_reference) list -> tactic
 val unfold_in_hyp     : 
   (int list * evaluable_global_reference) list -> hyp_location -> tactic
@@ -250,3 +251,4 @@ val generalize_dep              : constr  -> tactic
 val tclABSTRACT : identifier option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic
+
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 3ee0ee430..1c95f7fdc 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -28,7 +28,7 @@ type 'a t = (global_reference,constr_pattern,'a) Dn.t
 let decomp = 
   let rec decrec acc c = match kind_of_term c with
     | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
-    | Cast (c1,_) -> decrec acc c1
+    | Cast (c1,_,_) -> decrec acc c1
     | _ -> (c,acc)
   in 
   decrec []