diff options
author | 2001-06-29 15:36:34 +0000 | |
---|---|---|
committer | 2001-06-29 15:36:34 +0000 | |
commit | 6ef77192c01e985fc9b106990f3109b399683e6a (patch) | |
tree | d40f4518100a2e943cf2eb7e1090eeaf5962cd92 /proofs/clenv.ml | |
parent | 78063364202264370e7a014fa21e527fb0614996 (diff) |
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
Diffstat (limited to 'proofs/clenv.ml')
-rw-r--r-- | proofs/clenv.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 70f4f7080..94d3c1b69 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 |