Suppression des warnings a la compilation de contrib/linear

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

2 files changed, 52 insertions, 28 deletions

diff --git a/contrib/linear/ccidpc.ml4 b/contrib/linear/ccidpc.ml4
index 1e3ec39e4..1823b2d48 100755
--- a/contrib/linear/ccidpc.ml4
+++ b/contrib/linear/ccidpc.ml4
@@ -105,8 +105,9 @@ let ctr = ref 0
 let gen_ident id = make_ident (atompart_of_id id) (incr ctr;Some !ctr)
 
 let gen_name a na =
-    let (Name id) = (named_hd Environ.empty_env a na)
-    in gen_ident id
+    match (named_hd Environ.empty_env a na) with 
+	(Name id)->gen_ident id
+      | Anonymous->assert false
 
 let dpc_of_cci_term lid = 
  let rec tradrec cciterm =
@@ -140,6 +141,7 @@ let cci_of_dpc_term tradsign sign =
     | APP (t::dpcargs) ->
 	let t' = tradrec t in
 	  Term.applist(t', List.map tradrec dpcargs)
+    | _-> assert false
   in tradrec
     
 
@@ -160,13 +162,13 @@ let dpc_of_cci_fmla gls cciterm =
     (match match_with_forall_term cciterm with
 	 Some ((na,a,b) as trp)->
 	   let id = gen_name a na in
-	   let f=mkApp(mkLambda trp,[|mkVar id|]) in
+	   let f=whd_beta (mkApp ((mkLambda trp),[|mkVar id|])) in
 	     ForAll(id,tradrec (id::lid) f)
        |_-> 
 	   (match match_with_exist_term cciterm with
 		Some ((na,a,b)as trp)->
 		  let id = gen_name a na in
-		  let f=mkApp(mkLambda trp,[|mkVar id|]) in
+		  let f=whd_beta (mkApp ((mkLambda trp),[|mkVar id|])) in
 		    Exists(id,tradrec (id::lid) f)
 	      |_->   
     let (hd,args) = whd_betaiota_stack cciterm in
@@ -209,7 +211,8 @@ let forAllI gls=if is_forall_term (pf_concl gls) then
 let forAllE id t gls =
   let rgl=pf_whd_betadeltaiota gls (pf_type_of gls (mkVar id)) in
     if is_forall_term rgl then
-      generalize [mkApp (mkVar id,[|t|])] gls else  tclFAIL 0 gls
+      tclTHEN (generalize [mkApp (mkVar id,[|t|])]) intro gls
+    else  tclFAIL 0 gls
 
 let existE id gls =
   let (_,_,t)=lookup_named id (pf_hyps gls) in
@@ -227,6 +230,11 @@ let negE id gls =
 (*t exist_intro_head = put_pat mmk "ex_intro"*)
 
 let existI t gls =
+(*  if is_exist_term (pf_concl gls) then
+    split (Rawterm.ImplicitBindings [t]) gls
+  else tclFAIL 0 gls *)
+    
+ 
     let (wc,kONT) = Evar_refiner.startWalk gls in
     let clause = mk_clenv_hnf_constr_type_of wc (pf_concl gls) in
     let clause' = clenv_constrain_missing_args [t] clause
@@ -340,8 +348,9 @@ let rec tradpf kspine jspine dpcpf gls =
   | Proof2(_,_,LExists2(kid,f,pf)) ->
     let id = find_fmla_left (kspine,Exists(kid,f)) (jspine,gls)
     in ((tclTHEN (existE id)
-        ((onNthClause (fun (Some jid) ->
-                          trad (kid::kspine) (jid::jspine) pf)
+        ((onNthClause (function (Some jid) ->
+                          trad (kid::kspine) (jid::jspine) pf
+			 | None-> assert false)
          (-2))))) gls
 
   | Proof2(_,_,RExists2(kid,kterm,f,pf)) ->
@@ -368,4 +377,4 @@ and trad kspine jspine dpcpf gls =
     tradpf kspine jspine dpcpf gls
 
 
-(* $Id$ *)
+
diff --git a/contrib/linear/lk_proofs.ml b/contrib/linear/lk_proofs.ml
index e4ee29807..1360615a4 100755
--- a/contrib/linear/lk_proofs.ml
+++ b/contrib/linear/lk_proofs.ml
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-open Names
+open Names 
 
 open General
 open Dpctypes
@@ -106,6 +106,7 @@ let sep_at at llt (lmu,_) =
       	       	    then ((Po a)::l1,l2)
 		    else (l1,(Po a)::l2)
     | [] -> ([],[])
+    | _->assert false 
   in sep_at_rec at
      
 let sep_nat nat llt (lmu,_) = 
@@ -117,6 +118,7 @@ let sep_nat nat llt (lmu,_) =
       	       	    then ((No a)::l1,l2)
 		    else (l1,(No a)::l2)
     | [] -> ([],[])
+    | _->assert false 
   in sep_nat_rec nat
 
 let sep_neg neg llt (lmu,_) = 
@@ -193,6 +195,7 @@ let sep_path (at,nat,conj,rneg,lneg) p =
       [x] -> x
     | ((Po(Conj _),_,_) as c::_) -> c     (** on recherche d'abord A/\B **)
     | _::ll -> find_X0 ll
+    | _->assert false 
   in let (x0,l1,l2) = if all_X0=[] then 
                        failwith "Can't find X0 in sep_path ! (impossible case)"
                       else find_X0 all_X0
@@ -206,7 +209,9 @@ let sep_path (at,nat,conj,rneg,lneg) p =
   in let litS1 = glue (List.map (fun x -> all_lit_sfla x) s1)
   in let (at1,at2) = sep_at at litS1 p
      and (nat1,nat2) = sep_nat nat litS1 p
-  in let neg = lneg @ (List.map (fun (Po (Neg f)) -> (No f)) rneg)
+  in let neg = lneg @ (List.map (function 
+				     (Po (Neg f)) -> (No f) 
+				   | _->assert false) rneg)
   in let (neg1,neg2) = sep_neg neg litS1 p
   in let lit_at1 = List.map proj at1
      and lit_nat1 = List.map proj nat1
@@ -241,11 +246,15 @@ let rec rneg_case pr = function
 	     and sq2' = (Neg f)::sq2
 	  in (Proof2(sq1',sq2',RNeg2(f,pr1)))
    | [] -> pr
+   | _->assert false 
 
-let lneg_case ((Proof2(sq1,sq2,_)) as pr) (No(Neg f)) = 
-   let sq1' = (Neg f)::sq1
-   and sq2' = substract sq2 [f]
-   in (Proof2(sq1',sq2',LNeg2(f,pr)))
+
+let lneg_case ((Proof2(sq1,sq2,_)) as pr) =function 
+    (No(Neg f))-> 
+      let sq1' = (Neg f)::sq1
+      and sq2' = substract sq2 [f]
+      in (Proof2(sq1',sq2',LNeg2(f,pr)))
+  | _->assert false 
 
 let find_lneg lneg = 
   let rec is_negneg = function
@@ -296,14 +305,18 @@ and cases (at,nat,conj,rneg,lneg) p =
       in rneg_case pr rneg
    else
       if rneg<>[] then
-      	 let s = at@nat@lneg@(List.map (fun (Po (Neg f)) -> (No f)) rneg)
+      	 let s = at@nat@lneg@(List.map (function 
+					    (Po (Neg f)) -> (No f)
+				          | _->assert false) rneg)
 	 in let pr = proof_of_path s p
 	 in rneg_case pr rneg
       else 
-      	 let (No (Neg f)) as g = find_lneg lneg
-	 in let s = at@nat@(substract lneg [g])@[Po f]
-	 in let pr = proof_of_path s p
-	 in lneg_case pr g
+	match find_lneg lneg with 
+	    (No (Neg f)) as g ->
+      	      let s = at@nat@(substract lneg [g])@[Po f] in
+	      let pr = proof_of_path s p in
+		lneg_case pr g
+	  |_->assert false
 
 
 (* pi_formula : separated formula -> formula 
@@ -718,13 +731,15 @@ let int_quant f u pr =
      let qt = quant_var f
   in let un_qt = such_that qt (function (Universal _) -> true | _ -> false)
      and fr_var = free_var_formula f
-  in let un_var = List.map (fun (Universal(id,_,_)) -> id) un_qt
-  in let sk_var  = un_var @ fr_var
-  in let u0 = unher_unif sk_var u
-  in let pr0 = pi_proof pr
-  in let pr1 = unher_proof sk_var pr0
-  in let cst = make_constraints qt u0
-  in let pog = make_pog qt cst
-  in let qpr = quant_proof cst pog pr1
-  in witness_proof u0 qpr
+     in let un_var = List.map (function 
+				   (Universal(id,_,_)) -> id
+				 | _ ->assert false) un_qt
+     in let sk_var  = un_var @ fr_var
+     in let u0 = unher_unif sk_var u
+     in let pr0 = pi_proof pr
+     in let pr1 = unher_proof sk_var pr0
+     in let cst = make_constraints qt u0
+     in let pog = make_pog qt cst
+     in let qpr = quant_proof cst pog pr1
+     in witness_proof u0 qpr