Fixing Derive Inversion for new proof engine

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

3 files changed, 18 insertions, 5 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 000c062832..f63c01a3ef 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -349,6 +349,16 @@ let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty =
   evdref := evd';
   ev
 
+(* This assumes an evar with identity instance and generalizes it over only 
+   the de Bruijn part of the context *)
+let generalize_evar_over_rels sigma (ev,args) =
+  let evi = Evd.find sigma ev in
+  let sign = named_context_of_val evi.evar_hyps in
+  List.fold_left2
+    (fun (c,inst as x) a d ->
+      if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
+     (evi.evar_concl,[]) (Array.to_list args) sign
+
 (*------------------------------------*
  * operations on the evar constraints *
  *------------------------------------*)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index cbdc20f92a..e21516681b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -198,3 +198,5 @@ val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
 
 val push_rel_context_to_named_context : Environ.env -> types -> 
   named_context_val * types * constr list
+
+val generalize_evar_over_rels : evar_map -> existential -> types * constr list
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 5c22bfd894..abb114d917 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -229,16 +229,17 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let { sigma=sigma } = Proof.V82.subgoals pf in
   let rec fill_holes c =
     match kind_of_term c with
-    | Evar (e,_) ->
+    | Evar (e,args) ->
 	let h = next_ident_away (id_of_string "H") !avoid in
-	let ty = (Evd.find sigma e).evar_concl in
+	let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
 	avoid := h::!avoid;
 	ownSign := add_named_decl (h,None,ty) !ownSign;
-	mkVar h
+	applist (mkVar h, inst)
     | _ -> map_constr fill_holes c
   in
-  let invProof =
-    it_mkNamedLambda_or_LetIn (fill_holes pfterm) !ownSign
+  let c = fill_holes pfterm in
+  (* warning: side-effect on ownSign *)
+  let invProof = it_mkNamedLambda_or_LetIn c !ownSign
   in
   invProof