Ajout (pour complétude) du cas d'inversion d'un pattern de Miller vis

à vis d'une Var nommée.



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

1 files changed, 6 insertions, 3 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c4c5ec9223..73cfa698db 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -503,9 +503,12 @@ let is_unification_pattern (_,args) l =
 let solve_pattern_eqn env l1 c =
   let c' = List.fold_right (fun a c ->
     let c' = subst_term (lift 1 a) (lift 1 c) in
-    let n = destRel a in 
-    let (na,_,t) = lookup_rel n env (* if na defined, do as if assumption *) in
-    (mkLambda (na,lift n t,c'))) l1 c in
+    match kind_of_term a with
+      (* Rem: if [a] links to a let-in, do as if it were an assumption *)
+      | Rel n -> let (na,_,t) = lookup_rel n env in mkLambda (na,lift n t,c')
+      | Var id -> let (id,_,t) = lookup_named id env in mkNamedLambda id t c'
+      | _ -> assert false) 
+    l1 c in
   whd_eta c'
 
 (* This code (i.e. solve_pb, etc.) takes a unification