backtrack unification types et deplacement make_clenv_binding

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

2 files changed, 43 insertions, 1 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 52ce2d2ea..f7ec08030 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 05baad0ca..dd8e9c31e 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