Ajout de la tactique "apply in".

Au passage, déplacement des tactiques cut and co plus en amont + commentaires.


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

2 files changed, 51 insertions, 3 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index b593411eaf..a0064b13b8 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -74,6 +74,26 @@ let clenv_get_type_of ce c =
       (meta_list ce.env) in
   Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
 
+exception NotExtensibleClause
+
+let clenv_push_prod cl =
+  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let rec clrec typ = match kind_of_term typ with
+    | Cast (t,_,_) -> clrec t
+    | Prod (na,t,u) ->
+	let mv = new_meta () in
+	let dep = dependent (mkRel 1) u in
+	let na' = if dep then na else Anonymous in
+	let e' = meta_declare mv t ~name:na' cl.env in
+	let concl = if dep then subst1 (mkMeta mv) u else u in
+	let def = applist (cl.templval.rebus,[mkMeta mv]) in
+	{ templval = mk_freelisted def;
+	  templtyp = mk_freelisted concl;
+	  env = e';
+	  templenv = cl.templenv }
+    | _ -> raise NotExtensibleClause
+  in clrec typ
+
 let clenv_environments evd bound c =
   let rec clrec (e,metas) n c =
     match n, kind_of_term c with
@@ -258,7 +278,20 @@ let connect_clenv gls clenv =
  * resolution can cause unification of already-existing metavars, and
  * of the fresh ones which get created.  This operation is a composite
  * of operations which pose new metavars, perform unification on
- * terms, and make bindings.  *)
+ * terms, and make bindings. 
+
+   Otherwise said, from 
+
+     [clenv] = [env;sigma;metas |- c:T]
+     [clenv'] = [env';sigma';metas' |- d:U]
+     [mv] = [mi] of type [Ti] in [metas]
+
+   then, if the unification of [Ti] and [U] produces map [rho], the
+   chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for
+   [rho'] being [rho;mi:=d].
+
+   In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
+*)
 let clenv_fchain mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
@@ -422,7 +455,7 @@ let make_clenv_binding_gen n gls (c,t) = function
   | NoBindings ->
       mk_clenv_from_n gls n (c,t)
 
-let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
+let make_clenv_binding_apply gls n = make_clenv_binding_gen (Some n) gls
 let make_clenv_binding = make_clenv_binding_gen None
 
 (****************************************************************)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index b1f08a6916..53a106ade5 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -105,12 +105,27 @@ val make_clenv_binding_apply :
 val make_clenv_binding :
   evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv
 
-(* other stuff *)
+(* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
+   [lmetas] is a list of metas to be applied to a proof of [t] so that
+   it produces the unification pattern [ccl]; [sigma'] is [sigma]
+   extended with [lmetas]; if [n] is defined, it limits the size of
+   the list even if [ccl] is still a product; otherwise, it stops when
+   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
+   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
+   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
+   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
 val clenv_environments :
  evar_defs -> int option -> types -> evar_defs * constr list * types
+
+(* [clenv_environments_evars env sigma n t] does the same but returns
+   a list of Evar's defined in [env] and extends [sigma] accordingly *)
 val clenv_environments_evars :
  env -> evar_defs -> int option -> types -> evar_defs * constr list * types
 
+(* if the clause is a product, add an extra meta for this product *)
+exception NotExtensibleClause
+val clenv_push_prod : clausenv -> clausenv
+
 (***************************************************************)
 (* Pretty-print *)
 val pr_clenv : clausenv -> Pp.std_ppcmds