Autoriser Apply avec un but sous forme d'implication ou de quantification

universelle


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

2 files changed, 11 insertions, 2 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 70f4f70802..94d3c1b692 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -352,6 +352,14 @@ let clenv_environments bound c =
   in 
   clrec (Intmap.empty,Intmap.empty,[]) bound c
 
+let mk_clenv_from_n wc n (c,cty) =
+  let (namenv,env,args,concl) = clenv_environments n cty in
+  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
+    templtyp = mk_freelisted concl;
+    namenv = namenv;
+    env = env;
+    hook = wc }
+
 let mk_clenv_from wc (c,cty) =
   let (namenv,env,args,concl) = clenv_environments (-1) cty in
   { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
@@ -1060,11 +1068,11 @@ let e_res_pf kONT clenv gls =
 let collect_com lbind = 
   map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind
 
-let make_clenv_binding_apply wc (c,t) lbind = 
+let make_clenv_binding_apply wc n (c,t) lbind = 
   let largs = collect_com lbind in
   let lcomargs = List.length largs in
   if lcomargs = List.length lbind then 
-    let clause = mk_clenv_from wc (c,t) in
+    let clause = mk_clenv_from_n wc n (c,t) in
     clenv_constrain_missing_args largs clause
   else if lcomargs = 0 then 
     let clause = mk_clenv_rename_from wc (c,t) in
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 106369d330..20eae81114 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -97,6 +97,7 @@ val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
 
 val make_clenv_binding_apply :
   walking_constraints ->
+  int ->
   constr * constr ->
   (bindOcc * types) list ->
   walking_constraints clausenv