diff options
| -rw-r--r-- | proofs/clenv.ml | 33 | ||||
| -rw-r--r-- | proofs/clenv.mli | 11 | ||||
| -rw-r--r-- | tactics/tactics.ml | 29 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 |
4 files changed, 43 insertions, 34 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 52ce2d2ea0..f7ec080301 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -605,7 +605,7 @@ let clenv_unify_core with_types m n clenv = clenv_merge with_types mc ec clenv (* let clenv_unify = clenv_unify_core false *) -let clenv_unify = clenv_unify_core true +let clenv_unify = clenv_unify_core false let clenv_typed_unify = clenv_unify_core true (* [clenv_bchain mv clenv' clenv] @@ -1042,6 +1042,37 @@ let e_res_pf kONT clenv gls = clenv_refine kONT (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls +(* Clausal environment for an application *) + +let collect_com lbind = + map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind + +let make_clenv_binding_apply wc (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 + clenv_constrain_missing_args largs clause + else if lcomargs = 0 then + let clause = mk_clenv_rename_from wc (c,t) in + clenv_match_args lbind clause + else + errorlabstrm "make_clenv_bindings" + [<'sTR "Cannot mix bindings and free associations">] + +let make_clenv_binding wc (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 + clenv_constrain_dep_args largs clause + else if lcomargs = 0 then + let clause = mk_clenv_rename_from wc (c,t) in + clenv_match_args lbind clause + else + errorlabstrm "make_clenv_bindings" + [<'sTR "Cannot mix bindings and free associations">] + open Printer let pr_clenv clenv = diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 05baad0ca1..dd8e9c31e8 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -78,6 +78,17 @@ val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic val clenv_type_of : wc clausenv -> constr -> constr val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv +val make_clenv_binding_apply : + walking_constraints -> + constr * constr -> + (bindOcc * types) list -> + walking_constraints clausenv +val make_clenv_binding : + walking_constraints -> + constr * constr -> + (bindOcc * types) list -> + walking_constraints clausenv + (* Exported for program.ml only *) val clenv_add_sign : (identifier * types) -> wc clausenv -> wc clausenv diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 82f4314456..424b785bc1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -465,22 +465,6 @@ let bring_hyps clsl gl = (* Resolution with missing arguments *) -let collect_com lbind = - map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind - -let make_clenv_binding_apply wc (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 - clenv_constrain_missing_args largs clause - else if lcomargs = 0 then - let clause = mk_clenv_rename_from wc (c,t) in - clenv_match_args lbind clause - else - errorlabstrm "make_clenv_bindings" - [<'sTR "Cannot mix bindings and free associations">] - let apply_with_bindings (c,lbind) gl = let (wc,kONT) = startWalk gl in let t = w_hnf_constr wc (w_type_of wc c) in @@ -955,19 +939,6 @@ let elimination_clause_scheme kONT wc elimclause indclause gl = (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and * refine fails *) -let make_clenv_binding wc (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 - clenv_constrain_dep_args largs clause - else if lcomargs = 0 then - let clause = mk_clenv_rename_from wc (c,t) in - clenv_match_args lbind clause - else - errorlabstrm "make_clenv_bindings" - [<'sTR "Cannot mix bindings and free associations">] - let type_clenv_binding wc (c,t) lbind = clenv_instance_template_type (make_clenv_binding wc (c,t) lbind) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0644bc972a..c81e1436f9 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -18,10 +18,6 @@ open Tacticals (*s General functions. *) -val make_clenv_binding_apply : - walking_constraints -> constr * constr -> constr substitution -> - walking_constraints clausenv - val type_clenv_binding : walking_constraints -> constr * constr -> constr substitution -> constr |