- install evar printer for debugging

- make unification try canonical structures before expansion as in evar_conv
- add a fast path to evar inversion (patch from B. Ziliani).


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

3 files changed, 23 insertions, 5 deletions

diff --git a/dev/include b/dev/include
index f785573ceb..9518034df1 100644
--- a/dev/include
+++ b/dev/include
@@ -44,6 +44,7 @@
 (*#install_printer  (* proof *)  pproof;;*)
 #install_printer  (* Goal.goal *)  ppgoalgoal;;
 #install_printer  (* metaset.t *) ppmetas;;
+#install_printer  (* evar *)  ppevar;;
 #install_printer  (* evar_map *)  ppevm;;
 #install_printer  (* Evar.Set.t *) ppexistentialset;;
 #install_printer  (* clenv *) ppclenv;;
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 288ec6214f..20a4a3f9e3 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -305,7 +305,7 @@ let remove_instance_local_defs evd evk args =
   let rec aux sign i = match sign with
   | [] ->
     let () = assert (i = len) in []
-  | (_, None _, _) :: sign ->
+  | (_, None, _) :: sign ->
     let () = assert (i < len) in
     (Array.unsafe_get args i) :: aux sign (succ i)
   | (_, Some _, _) :: sign ->
@@ -1248,8 +1248,25 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
               imitate envk t in
 
   let rhs = whd_beta evd rhs (* heuristic *) in
-  let body = imitate (env,0) rhs in
-  (!evdref,body)
+  let fast rhs = 
+    let filter_ctxt = evar_filtered_context evi in
+    let names = ref Idset.empty in
+    let rec is_id_subst ctxt s =
+      match ctxt, s with
+      | ((id, _, _) :: ctxt'), (c :: s') ->
+        names := Idset.add id !names;
+        isVarId id c && is_id_subst ctxt' s'
+      | [], [] -> true
+      | _ -> false 
+    in
+      is_id_subst filter_ctxt (Array.to_list argsv) &&
+      closed0 rhs &&
+      Idset.subset (collect_vars rhs) !names 
+  in
+  let body =
+    if fast rhs then nf_evar evd rhs
+    else imitate (env,0) rhs
+ in (!evdref,body)
 
 (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
  * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b9b076d4fd..9c3b5c4dff 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -503,9 +503,9 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
     with ex when precatchable_exception ex ->
     try reduce curenvnb pb b false substn cM cN
     with ex when precatchable_exception ex ->
-    try expand curenvnb pb b false substn cM f1 l1 cN f2 l2
+    try canonical_projections curenvnb pb b cM cN substn
     with ex when precatchable_exception ex ->
-    canonical_projections curenvnb pb b cM cN substn
+    expand curenvnb pb b false substn cM f1 l1 cN f2 l2
 
   and unify_not_same_head curenvnb pb b wt substn cM cN =
     try canonical_projections curenvnb pb b cM cN substn