Correct handling of the environment in build_signature, and throw

exception for dependent arrow types.


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

1 files changed, 6 insertions, 4 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 29f0d0766..afefeabb3 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -524,11 +524,13 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
 	    new_evar isevars env relty
       | Some x -> f x
   in
-  let rec aux ty l =
+  let rec aux env ty l =
     let t = Reductionops.whd_betadeltaiota env (Evd.evars_of !isevars) ty in
-    match kind_of_term t, l with
+      match kind_of_term t, l with
       | Prod (na, ty, b), obj :: cstrs -> 
-	  let (b, arg, evars) = aux b cstrs in
+	  if dependent (mkRel 1) ty then 
+	    raise (Invalid_argument "build_signature: cannot handle dependent morphisms");
+	  let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in
 	  let ty = Reductionops.nf_betaiota ty in
 	  let relty = mk_relty ty obj in
 	  let arg' = mkApp (Lazy.force respectful, [| ty ; b ; relty ; arg |]) in
@@ -542,7 +544,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
 		  t, rel, [t, rel]
 	    | Some codom -> let (t, rel) = Lazy.force codom in
 			      t, rel, [t, rel])
-  in aux m cstrs
+  in aux env m cstrs
 
 let morphism_proof env evars carrier relation x =
   let goal =