finalized suffices

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

3 files changed, 75 insertions, 39 deletions

diff --git a/.depend b/.depend
index 7866da407f..12db266e17 100644
--- a/.depend
+++ b/.depend
@@ -533,7 +533,7 @@ dev/top_printers.cmo: toplevel/vernacinterp.cmi lib/util.cmi kernel/univ.cmi \
     pretyping/termops.cmi kernel/term.cmi parsing/tactic_printer.cmi \
     lib/system.cmi kernel/sign.cmi proofs/refiner.cmi proofs/proof_trees.cmi \
     parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi proofs/pfedit.cmi \
-    parsing/pcoq.cmi kernel/names.cmi library/nameops.cmi \
+    parsing/pcoq.cmi lib/options.cmi kernel/names.cmi library/nameops.cmi \
     kernel/mod_subst.cmi proofs/logic.cmi library/libobject.cmi \
     library/libnames.cmi library/goptions.cmi library/global.cmi \
     interp/genarg.cmi pretyping/evd.cmi kernel/environ.cmi \
@@ -544,7 +544,7 @@ dev/top_printers.cmx: toplevel/vernacinterp.cmx lib/util.cmx kernel/univ.cmx \
     pretyping/termops.cmx kernel/term.cmx parsing/tactic_printer.cmx \
     lib/system.cmx kernel/sign.cmx proofs/refiner.cmx proofs/proof_trees.cmx \
     parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx proofs/pfedit.cmx \
-    parsing/pcoq.cmx kernel/names.cmx library/nameops.cmx \
+    parsing/pcoq.cmx lib/options.cmx kernel/names.cmx library/nameops.cmx \
     kernel/mod_subst.cmx proofs/logic.cmx library/libobject.cmx \
     library/libnames.cmx library/goptions.cmx library/global.cmx \
     interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 466596d24a..0a984cceb9 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -34,6 +34,9 @@ let intern_statement intern_it globs st =
   {st_label=st.st_label;
    st_it=intern_it globs st.st_it}
     
+let intern_no_bind intern_it globs x =
+  globs,intern_it globs x
+
 let intern_constr_or_thesis globs = function
     Thesis n -> Thesis n
   | This c -> This (intern_constr globs c)
@@ -57,13 +60,15 @@ let intern_hyps iconstr globs hyps =
   snd (list_fold_map (intern_hyp iconstr) globs hyps)
 
 let intern_cut intern_it globs cut=
- {cut_stat=intern_it globs cut.cut_stat;
-  cut_by=intern_justification_items globs cut.cut_by;
-  cut_using=intern_justification_method globs cut.cut_using}
+  let nglobs,nstat=intern_it globs cut.cut_stat in
+    {cut_stat=nstat;
+     cut_by=intern_justification_items nglobs cut.cut_by;
+     cut_using=intern_justification_method nglobs cut.cut_using}
 
 let intern_casee globs = function 
     Real c -> Real (intern_constr globs c)
-  | Virtual cut -> Virtual (intern_cut (intern_statement intern_constr) globs cut) 
+  | Virtual cut -> Virtual 
+      (intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut) 
 
 let intern_hyp_list args globs =
   let intern_one globs (loc,(id,opttyp)) =
@@ -73,7 +78,7 @@ let intern_hyp_list args globs =
 
 let intern_suffices_clause globs (hyps,c) = 
   let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in
-    (nhyps,intern_constr_or_thesis nglobs c) 
+    nglobs,(nhyps,intern_constr_or_thesis nglobs c) 
 
 let intern_fundecl args body globs= 
   let nglobs,nargs = intern_hyp_list args globs in
@@ -98,10 +103,14 @@ let rec intern_bare_proof_instr globs = function
     Pthus i -> Pthus (intern_bare_proof_instr globs i)
   | Pthen i -> Pthen (intern_bare_proof_instr globs i)
   | Phence i -> Phence (intern_bare_proof_instr globs i)
-  | Pcut c -> Pcut (intern_cut (intern_statement intern_constr_or_thesis) globs c)
+  | Pcut c -> Pcut 
+      (intern_cut 
+	 (intern_no_bind (intern_statement intern_constr_or_thesis)) globs c)
   | Psuffices c -> 
       Psuffices (intern_cut intern_suffices_clause globs c)
-  | Prew (s,c) -> Prew (s,intern_cut (intern_statement intern_constr) globs c) 
+  | Prew (s,c) -> Prew 
+      (s,intern_cut 
+	 (intern_no_bind  (intern_statement intern_constr)) globs c) 
   | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps)
   | Pcase (params,pat,hyps) -> 
       let nglobs,nparams = intern_hyp_list params globs in
@@ -382,20 +391,34 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	     pat_expr=pat},thyps
 
 let interp_cut interp_it sigma env cut=
-  {cut with 
-    cut_stat=interp_it sigma env cut.cut_stat;
-    cut_by=interp_justification_items sigma env cut.cut_by}
+  let nenv,nstat = interp_it sigma env cut.cut_stat in
+    {cut with 
+       cut_stat=nstat;
+       cut_by=interp_justification_items sigma nenv cut.cut_by}
+
+let interp_no_bind interp_it sigma env x =
+  env,interp_it sigma env x
 
 let interp_suffices_clause sigma env (hyps,cot)=
-  match cot with
-      This (c,_) -> 
-	let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in nhyps,This nc
-    | Thesis (Plain| Sub _) as th  -> interp_hyps sigma env hyps,th
-      | Thesis (For n) -> error "\"thesis for\" is not applicable here"
- 
+  let (locvars,_) as res =
+    match cot with
+	This (c,_) -> 
+	  let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in
+	  nhyps,This nc
+      | Thesis (Plain| Sub _) as th  -> interp_hyps sigma env hyps,th
+      | Thesis (For n) -> error "\"thesis for\" is not applicable here" in
+  let push_one hyp env0 =
+    match hyp with
+	(Hprop st | Hvar st) ->
+	  match st.st_label with
+	      Name id -> Environ.push_named (id,None,st.st_it) env0
+	    | _ -> env in
+  let nenv = List.fold_right push_one locvars env in 
+    nenv,res 
+	  
 let interp_casee sigma env = function 
     Real c -> Real (understand sigma env (fst c))
-  | Virtual cut -> Virtual (interp_cut (interp_statement (interp_constr true)) sigma env cut) 
+  | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut) 
 
 let abstract_one_arg = function
     (loc,(id,None)) ->
@@ -417,12 +440,15 @@ let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = fu
     Pthus i -> Pthus (interp_bare_proof_instr info sigma env i)
   | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i)
   | Phence i -> Phence (interp_bare_proof_instr info sigma env i)
-  | Pcut c -> Pcut (interp_cut (interp_statement (interp_constr_or_thesis true)) sigma env c) 
+  | Pcut c -> Pcut (interp_cut 
+		      (interp_no_bind (interp_statement 
+					 (interp_constr_or_thesis true))) 
+		      sigma env c) 
   | Psuffices c ->  
       Psuffices (interp_cut interp_suffices_clause sigma env c)
-
   | Prew (s,c) -> Prew (s,interp_cut 
-			  (interp_statement (interp_constr_in_type (get_eq_typ info env)))
+			  (interp_no_bind (interp_statement 
+			     (interp_constr_in_type (get_eq_typ info env))))
 			  sigma env c) 
 
   | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps)
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index e2e8a19274..8a22e8b8d9 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -350,10 +350,11 @@ let enstack_subsubgoals env se stack gls=
 	    Array.iteri process gentypes
       | _ -> ()
 
-let find_subsubgoal env c ctyp skip evd metas gls =
+let find_subsubgoal env c ctyp skip evd metas submetas gls =
   let stack = Stack.create () in
   let max_meta = 
-    List.fold_left (fun a (m,_) -> max a m) 0 metas in
+    let tmp = List.fold_left (fun a (m,_) -> max a m) 0 metas in
+      List.fold_left (fun a (m,_) -> max a m) tmp submetas in
   let _ = 
     List.iter (fun (m,typ) -> 
 		 Stack.push 
@@ -369,7 +370,10 @@ let find_subsubgoal env c ctyp skip evd metas gls =
 	  Unification.w_unify true env Reduction.CUMUL 
 	    ctyp se.se_type se.se_evd in
 	  if n <= 0 then 
-	      {se with se_evd=meta_assign se.se_meta (c,ConvUpToEta 0) unifier}
+	      {se with 
+		 se_evd=meta_assign se.se_meta (c,ConvUpToEta 0) unifier;
+	         se_meta_list=replace_in_list 
+		  se.se_meta submetas se.se_meta_list}
 	  else
 	      dfs (pred n)
       with _ -> 
@@ -389,7 +393,6 @@ let rec nf_list evd =
 	else
 	  (m,nf_meta evd typ)::nf_list evd others
 
-
 let rec max_linear_context meta_one c =
   if !meta_one = None then
      if isMeta c then
@@ -411,12 +414,12 @@ let rec max_linear_context meta_one c =
     else
       map_constr (max_linear_context meta_one) c
 
-let thus_tac c ctyp gls =  
+let thus_tac c ctyp submetas gls =  
   let info = get_its_info gls in
-  let evd0 = mk_evd info.pm_subgoals gls in
+  let evd0 = mk_evd (info.pm_subgoals@submetas) gls in
   let list,evd = 
     try
-      find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals gls
+      find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals submetas gls
     with Not_found -> 
       error "I could not relate this statement to the thesis" in
   let nflist = nf_list evd list in
@@ -489,7 +492,7 @@ let instr_cut mkstat _thus _then cut gls0 =
   let c_stat = mkstat info stat.st_it in
   let thus_tac gls= 
     if _thus then 
-      thus_tac (mkVar c_id) c_stat gls
+      thus_tac (mkVar c_id) c_stat [] gls
     else tclIDTAC gls in
     tclTHENS (internal_cut c_id c_stat) 
       [tclTHEN tcl_erase_info (just_tac _then cut info);
@@ -537,7 +540,7 @@ let instr_rew _thus rew_side cut gls0 =
     | Name id -> id,true in
   let thus_tac new_eq gls= 
     if _thus then 
-      thus_tac (mkVar c_id) new_eq gls
+      thus_tac (mkVar c_id) new_eq [] gls
     else tclIDTAC gls in
     match rew_side with 
 	Lhs ->
@@ -566,7 +569,7 @@ let instr_claim _thus st gls0 =
     | Name id -> id,true in
   let thus_tac gls= 
     if _thus then 
-      thus_tac (mkVar id) st.st_it gls
+      thus_tac (mkVar id) st.st_it [] gls
     else tclIDTAC gls in
   let ninfo1 = {info with 
 		  pm_stack=
@@ -653,7 +656,7 @@ let free_meta info =
 
 let rec metas_from n hyps = 
   match hyps with
-      _ :: q -> mkMeta n :: metas_from (succ n) q
+      _ :: q -> n :: metas_from (succ n) q
     | [] -> []
  
 let rec build_product args body =
@@ -662,21 +665,28 @@ let rec build_product args body =
 	let pprod= lift 1 (build_product rest body) in
 	let lbody =
 	  match st.st_label with
-	      Anonymous -> body
+	      Anonymous -> pprod
 	    | Name id -> subst_term (mkVar id) pprod in
 	  mkProd (st.st_label, st.st_it, lbody)
     | [] -> body 
 
+let rec build_applist prod = function
+    [] -> [],prod
+  | n::q -> 
+      let (_,typ,_) = destProd prod in
+      let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in
+	(n,typ)::ctx,head
+
 let instr_suffices _then cut gls0 = 
   let info = get_its_info gls0 in 
   let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in 
   let ctx,hd = cut.cut_stat in
   let c_stat = build_product ctx (mk_stat_or_thesis info hd) in
   let metas = metas_from (free_meta info) ctx in
-  let c_costat = prod_applist c_stat metas in
-  let costat = applist (mkVar c_id,metas) in  
- let thus_tac gls= 
-      thus_tac costat c_costat gls in
+  let c_ctx,c_head = build_applist c_stat metas in
+  let c_term = applist (mkVar c_id,List.map mkMeta metas) in  
+  let thus_tac gls= 
+    thus_tac c_term c_head c_ctx gls in
    tclTHENS (internal_cut c_id c_stat) 
      [tclTHENLIST 
 	 [ tcl_change_info 
@@ -799,7 +809,7 @@ let rec take_tac wits gls =
       [] -> tclIDTAC gls
     | wit::rest ->  
 	let typ = pf_type_of gls wit in  
-	  tclTHEN (thus_tac wit typ) (take_tac rest)  gls
+	  tclTHEN (thus_tac wit typ []) (take_tac rest)  gls
 
 
 (* tactics for define *)