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, 29 insertions, 24 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 1acf41ec6c..e0d877b66e 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -217,7 +217,7 @@ let subst_constr_expr a loc subs =
   | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l) 
   | CApp (_,(p,a),l) ->
       CApp (loc,(p,subst a),List.map (fun (a,i) -> (subst a,i)) l)
-  | CCast (_,a,b) -> CCast (loc,subst a,subst b)
+  | CCast (_,a,k,b) -> CCast (loc,subst a,k,subst b)
   | CNotation (_,n,l) -> CNotation (loc,n,List.map subst l)
   | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 1a509b1e10..722703c1fa 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -63,7 +63,7 @@ let set_loc loc = function
   | CPatVar(_,v) -> CPatVar(loc,v)
   | CEvar(_,ev) -> CEvar(loc,ev)
   | CSort(_,s) -> CSort(loc,s)
-  | CCast(_,a,b) -> CCast(loc,a,b)
+  | CCast(_,a,k,b) -> CCast(loc,a,k,b)
   | CNotation(_,n,l) -> CNotation(loc,n,l)
   | CNumeral(_,i) -> CNumeral(loc,i)
   | CDelimiters(_,s,e) -> CDelimiters(loc,s,e)
@@ -162,7 +162,8 @@ GEXTEND Gram
 *)
       | f = operconstr; args = LIST1 constr91 -> CApp (loc, (None,f), args) ]
     | "9" RIGHTA
-      [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> CCast (loc, c1, c2) ]
+      [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> 
+	CCast (loc, c1, Term.DEFAULTcast,c2) ]
     | "8" RIGHTA
       [ c1 = operconstr; "->"; c2 = operconstr LEVEL "8"-> CArrow (loc, c1, c2) ]
     | "1" RIGHTA
@@ -303,7 +304,7 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   opt_casted_constr:
-    [ [ c = constr;  ":"; t = constr -> CCast (loc, c, t)
+    [ [ c = constr;  ":"; t = constr -> CCast (loc, c, DEFAULTcast, t)
       | c = constr -> c ] ]
   ;
   vardecls:
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 0111dbaf80..d2df2e144e 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -33,7 +33,7 @@ let _ = Lexer.add_token ("","!")
 
 let mk_cast = function
     (c,(_,None)) -> c
-  | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, ty)
+  | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, DEFAULTcast,ty)
 
 let mk_lam = function
     ([],c) -> c
@@ -168,8 +168,8 @@ GEXTEND Gram
     [ "200" RIGHTA
       [ c = binder_constr -> c ]
     | "100" RIGHTA
-      [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,c2)
-      | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,c2) ]
+      [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,DEFAULTcast,c2)
+      | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,DEFAULTcast,c2) ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
@@ -329,7 +329,7 @@ GEXTEND Gram
       | "("; id=name; ":="; c=lconstr; ")" ->
           LocalRawDef (id,c)
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
-          LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,t))
+          LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,DEFAULTcast,t))
     ] ]
   ;
   binder:
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index f482aa152e..4f25354b64 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -122,6 +122,6 @@ GEXTEND Gram
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
-      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,t) ] ]
+      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,Term.DEFAULTcast,t) ] ]
   ;
 END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 603abd73a7..0b4fc25f1e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -78,8 +78,8 @@ GEXTEND Gram
     ] ]
   ;
   constr_body:
-    [ [ ":="; c = constr; ":"; t = constr -> CCast(loc,c,t)
-      | ":"; t = constr; ":="; c = constr -> CCast(loc,c,t)
+    [ [ ":="; c = constr; ":"; t = constr -> CCast(loc,c,Term.DEFAULTcast,t)
+      | ":"; t = constr; ":="; c = constr -> CCast(loc,c,Term.DEFAULTcast,t)
       | ":="; c = constr -> c ] ]
   ;
   vernac_list_tail:
@@ -162,7 +162,7 @@ GEXTEND Gram
       | -> evar_constr loc ] ]
   ;
   opt_casted_constr:
-    [ [ c = constr;  ":"; t = constr -> CCast(loc,c,t)
+    [ [ c = constr;  ":"; t = constr -> CCast(loc,c,Term.DEFAULTcast,t)
       | c = constr -> c ] ]
   ;
   vardecls:
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 6277a9ab3f..70f28a2787 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -173,7 +173,7 @@ GEXTEND Gram
   def_body:
     [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr ->
       (match c with
-          CCast(_,c,t) -> DefineBody (bl, red, c, Some t)
+          CCast(_,c,k,t) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
       | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
           DefineBody (bl, red, c, Some t)
@@ -272,7 +272,7 @@ GEXTEND Gram
              t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t))
       | id = name; ":="; b = lconstr ->
          match b with
-             CCast(_,b,t) -> (false,DefExpr(id,b,Some t))
+             CCast(_,b,_,t) -> (false,DefExpr(id,b,Some t))
            | _ -> (false,DefExpr(id,b,None)) ] ]
   ;
   assum_list:
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 20506abcf0..02b35a1d81 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -151,7 +151,7 @@ let rec interp_xml_constr = function
       let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
       RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
   | XmlTag (loc,"CAST",al,[x1;x2]) ->
-      RCast (loc, interp_xml_term x1, interp_xml_type x2)
+      RCast (loc, interp_xml_term x1, DEFAULTcast, interp_xml_type x2)
   | XmlTag (loc,"SORT",al,[]) ->
       RSort (loc, get_xml_sort al)
   | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 37abe40633..c47ad04c34 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -315,7 +315,7 @@ let rec pr inherited a =
   | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_sort s, latom
-  | CCast (_,a,b) ->
+  | CCast (_,a,_,b) ->
       hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast
   | CNotation (_,"( _ )",[t]) ->
       str"("++ pr (max_int,E) t ++ str")", latom
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 0677f2699f..355bf6c941 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -405,7 +405,7 @@ let pr_prim_rule_v7 = function
       str(if occur_meta c then "Refine " else "Exact ") ++
       Constrextern.with_meta_as_hole print_constr c
       
-  | Convert_concl c ->
+  | Convert_concl (c,_) ->
       (str"Change "  ++ print_constr c)
       
   | Convert_hyp (id,None,t) ->
@@ -472,7 +472,7 @@ let pr_prim_rule_v8 = function
       str(if occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole print_constr8 c
       
-  | Convert_concl c ->
+  | Convert_concl (c,_) ->
       (str"change "  ++ print_constr8 c)
       
   | Convert_hyp (id,None,t) ->
diff --git a/parsing/search.ml b/parsing/search.ml
index ec7db48898..82829337a9 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -41,7 +41,7 @@ let rec head_const c = match kind_of_term c with
   | Prod (_,_,d) -> head_const d
   | LetIn (_,_,_,d) -> head_const d
   | App (f,_)   -> head_const f
-  | Cast (d,_)   -> head_const d
+  | Cast (d,_,_)   -> head_const d
   | _            -> c
 
 (* General search, restricted to head constant if [only_head] *)
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 942bce7987..6b5b35dd2a 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -53,12 +53,13 @@ let thin_sign osign sign =
        try 
 	 if Sign.lookup_named id osign = (id,c,ty) then sign
 	 else raise Different
-       with Not_found | Different -> add_named_decl d sign)
-    sign ~init:empty_named_context
+       with Not_found | Different -> Environ.push_named_context_val d sign)
+    sign ~init:Environ.empty_named_context_val
 
 let rec print_proof sigma osign pf =
   let {evar_hyps=hyps; evar_concl=cl; 
        evar_body=body} = pf.goal in
+  let hyps = Environ.named_context_of_val hyps in
   let hyps' = thin_sign osign hyps in
   match pf.ref with
     | None -> 
@@ -78,6 +79,7 @@ let pr_change gl =
 
 let rec print_script nochange sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
+  let sign = Environ.named_context_of_val sign in
   match pf.ref with
     | None ->
         (if nochange then 
@@ -124,10 +126,12 @@ let rec print_info_script sigma osign pf =
 		   (str "." ++ fnl ())
                  else 
 		   (str";" ++ brk(1,3) ++
-		      print_info_script sigma sign pf1)
+		      print_info_script sigma 
+		      (Environ.named_context_of_val sign) pf1)
              | _ -> (str"." ++ fnl () ++
                        prlist_with_sep pr_fnl
-                         (print_info_script sigma sign) spfl))
+                         (print_info_script sigma 
+			    (Environ.named_context_of_val sign)) spfl))
 
 let format_print_info_script sigma osign pf = 
   hov 0 (print_info_script sigma osign pf)
diff --git a/parsing/termast.ml b/parsing/termast.ml
index b4871598d0..3d191d4a9a 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -344,7 +344,7 @@ let rec ast_of_raw = function
 	 | RProp Pos -> ope("SET",[])
 	 | RType _ -> ope("TYPE",[]))
   | RHole _ -> ope("ISEVAR",[])
-  | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
+  | RCast (_,c,_,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
   | RDynamic (loc,d) -> Dynamic (loc,d)
 	
 and ast_of_eqn (_,ids,pl,c) =