Passage à des contextes de vars et de rels pouvant contenir des déclarations

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

12 files changed, 262 insertions, 268 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7de32f90f0..9b0d24632f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -239,9 +239,10 @@ let make_resolves name eap (c,cty) =
   ents
 
 (* used to add an hypothesis to the local hint database *)
-let make_resolve_hyp hname htyp = 
+let make_resolve_hyp (hname,_,htyp) = 
   try
-    [make_apply_entry (true, Options.is_verbose()) hname (mkVar hname, htyp)]
+    [make_apply_entry (true, Options.is_verbose()) hname
+       (mkVar hname, body_of_type htyp)]
   with 
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
@@ -596,12 +597,10 @@ let unify_resolve (c,clenv) gls =
   h_simplest_apply c gls
 
 (* builds a hint database from a constr signature *)
-(* typically used with (lid, ltyp) = pf_untyped_hyps <some goal> *)
+(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
 
 let make_local_hint_db sign = 
-  let hintlist =
-    list_map_append2 make_resolve_hyp
-      (ids_of_sign sign) (vals_of_sign sign) in
+  let hintlist = list_map_append make_resolve_hyp sign in
   Hint_db.add_list hintlist Hint_db.empty
 
 
@@ -617,8 +616,7 @@ let rec trivial_fail_db db_list local_db gl =
   let intro_tac = 
     tclTHEN intro 
       (fun g'->
-	 let (hn, htyp) = hd_sign (pf_untyped_hyps g') in
-	 let hintl = make_resolve_hyp hn htyp in
+	 let hintl = make_resolve_hyp (pf_last_hyp g') in
 	 trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
   in
   tclFIRST 
@@ -668,14 +666,13 @@ let trivial dbnames gl =
 	   error ("Trivial: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
-  tclTRY 
-    (trivial_fail_db db_list (make_local_hint_db (pf_untyped_hyps gl))) gl 
+  tclTRY (trivial_fail_db db_list (make_local_hint_db (pf_hyps gl))) gl 
     
 let full_trivial gl =
   let dbnames = stringmap_dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-  tclTRY (trivial_fail_db db_list (make_local_hint_db (pf_untyped_hyps gl))) gl
+  tclTRY (trivial_fail_db db_list (make_local_hint_db (pf_hyps gl))) gl
 
 let dyn_trivial = function
   | []                  -> trivial []
@@ -733,28 +730,26 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   (fun id -> tclTHEN (decomp_unary_term (VAR id)) 
 		(tclTHEN 
 		   (clear_one id)
-		   (search_gen decomp p db_list local_db nil_sign)))
-	   (ids_of_sign (pf_hyps goal))) 
+		   (search_gen decomp p db_list local_db [])))
+	   (pf_ids_of_hyps goal)) 
   in
   let intro_tac = 
     tclTHEN intro 
       (fun g' -> 
-	 let (hid,htyp) = hd_sign (pf_untyped_hyps g') in
+	 let (hid,_,htyp as d) = pf_last_hyp g' in
 	 let hintl = 
 	   try 
 	     [make_apply_entry (true,Options.is_verbose()) 
-		hid (mkVar hid,htyp)]
+		hid (mkVar hid,body_of_type htyp)]
 	   with Failure _ -> [] 
 	 in
-         search_gen decomp n db_list
-	   (Hint_db.add_list hintl local_db)
-	   (add_sign (hid,htyp) nil_sign) g') 
+         search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d] g') 
   in
   let rec_tacs = 
     List.map 
       (fun ntac -> 
 	 tclTHEN ntac
-	   (search_gen decomp (n-1) db_list local_db nil_sign))
+	   (search_gen decomp (n-1) db_list local_db empty_var_context))
       (possible_resolve db_list local_db (pf_concl goal))
   in 
   tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
@@ -774,7 +769,7 @@ let auto n dbnames gl =
 	   error ("Auto: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
-  let hyps = (pf_untyped_hyps gl) in
+  let hyps = pf_hyps gl in
   tclTRY (search n db_list (make_local_hint_db hyps) hyps) gl
 
 let default_auto = auto !default_search_depth []
@@ -783,7 +778,7 @@ let full_auto n gl =
   let dbnames = stringmap_dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-  let hyps = (pf_untyped_hyps gl) in
+  let hyps = pf_hyps gl in
   tclTRY (search n db_list (make_local_hint_db hyps) hyps) gl
   
 let default_full_auto gl = full_auto !default_search_depth gl
@@ -818,7 +813,7 @@ let h_auto = hide_tactic "Auto" dyn_auto
 let default_search_decomp = ref 1
 
 let destruct_auto des_opt n gl = 
-  let hyps = pf_untyped_hyps gl in
+  let hyps = pf_hyps gl in
   search_gen des_opt n [searchtable_map "core"] 
     (make_local_hint_db hyps) hyps gl
     
@@ -850,23 +845,23 @@ type autoArguments =
 
 let keepAfter tac1 tac2 = 
   (tclTHEN tac1 
-     (function g -> tac2 (make_sign [hd_sign (pf_untyped_hyps g)]) g))
+     (function g -> tac2 [pf_last_hyp g] g))
 
 let compileAutoArg contac = function
   | Destructing -> 
       (function g -> 
-         let ctx =(pf_untyped_hyps g) in  
+         let ctx = pf_hyps g in  
 	 tclFIRST 
-           (List.map2 
-              (fun id typ -> 
-                 if (Hipattern.is_conjunction (hd_of_prod typ)) then 
+           (List.map 
+              (fun (id,_,typ) -> 
+                 if (Hipattern.is_conjunction (hd_of_prod (body_of_type typ)))
+		 then 
 		   (tclTHEN
                       (tclTHEN (simplest_elim (mkVar id)) 
                          (clear_one id))
                       contac) 
                  else 
-		   tclFAIL 0)
-	      (ids_of_sign ctx) (vals_of_sign ctx)) g)
+		   tclFAIL 0) ctx) g)
   | UsingTDB ->  
       (tclTHEN  
          (Tacticals.tryAllClauses 
@@ -884,8 +879,9 @@ let rec super_search n db_list local_db argl goal =
      ::
      (tclTHEN intro 
         (fun g -> 
-	   let (hid,htyp) = hd_sign (pf_untyped_hyps g) in
-	   let hintl = make_resolves hid (true,false) (mkVar hid,htyp) in
+	   let (hid,_,htyp) = pf_last_hyp g in
+	   let hintl =
+	     make_resolves hid (true,false) (mkVar hid,body_of_type htyp) in
 	   super_search n db_list (Hint_db.add_list hintl local_db)
 	     argl g))
      ::
@@ -901,9 +897,11 @@ let rec super_search n db_list local_db argl goal =
 let search_superauto n ids argl g = 
   let sigma =
     List.fold_right
-      (fun id -> add_sign (id,pf_type_of g (pf_global g id)))
-      ids nil_sign in
-  let hyps = concat_sign (pf_untyped_hyps g) sigma in
+      (fun id -> add_var_decl
+	   (id,Retyping.get_assumption_of (pf_env g) (project g) 
+	      (pf_type_of g (pf_global g id))))
+      ids empty_var_context in
+  let hyps = List.append (pf_hyps g) sigma in
   super_search n [Stringmap.find "core" !searchtable] (make_local_hint_db hyps)
     argl g
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 50460de17a..b65d2ea218 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -85,8 +85,7 @@ val make_resolves :
    Never raises an User_exception;
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
-val make_resolve_hyp : identifier -> constr
-      -> (constr_label * pri_auto_tactic) list
+val make_resolve_hyp : var_declaration -> (constr_label * pri_auto_tactic) list
 
 (* [make_extern name pri pattern tactic_ast] *)
 
@@ -97,7 +96,7 @@ val make_extern :
 (* Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints *)
 
-val make_local_hint_db : constr signature -> Hint_db.t
+val make_local_hint_db : var_context -> Hint_db.t
 
 val priority : (int * 'a) list -> 'a list
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 74d49114ba..25bb62ab4c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -21,13 +21,13 @@ let e_give_exact c gl = tclTHEN (unify (pf_type_of gl c)) (Tactics.exact c) gl
 let assumption id = e_give_exact (VAR id)
         
 let e_assumption gl = 
-  tclFIRST (List.map assumption (ids_of_sign (pf_untyped_hyps gl))) gl
+  tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
 
 let e_give_exact_constr = hide_constr_tactic "EExact" e_give_exact
 
 let registered_e_assumption gl = 
   tclFIRST (List.map (fun id gl -> e_give_exact_constr (VAR id) gl) 
-              (ids_of_sign (pf_untyped_hyps gl))) gl
+              (pf_ids_of_hyps gl)) gl
     
 let e_resolve_with_bindings_tac  (c,lbind) gl = 
   let (wc,kONT) = startWalk gl in
@@ -54,9 +54,9 @@ let vernac_e_resolve_constr =
 let one_step l gl =
   [Tactics.intro]
   @ (List.map e_resolve_constr (List.map (fun x -> VAR x)
-				  (ids_of_sign (pf_untyped_hyps gl))))
+				  (pf_ids_of_hyps gl)))
   @ (List.map e_resolve_constr l)
-  @ (List.map assumption (ids_of_sign (pf_untyped_hyps gl)))
+  @ (List.map assumption (pf_ids_of_hyps gl))
 
 let rec prolog l n gl =
   if n <= 0 then error "prolog - failure";
@@ -152,8 +152,8 @@ let rec e_trivial_fail_db db_list local_db goal =
     registered_e_assumption ::
     (tclTHEN Tactics.intro 
        (function g'->
-	  let (hn,htyp) = hd_sign (pf_untyped_hyps g') in
-	  let hintl = make_resolve_hyp hn htyp in
+	  let d = pf_last_hyp g' in
+	  let hintl = make_resolve_hyp d in
           (e_trivial_fail_db db_list
 	     (Hint_db.add_list hintl local_db) g'))) ::
     (e_trivial_resolve db_list local_db (pf_concl goal)) 
@@ -223,14 +223,13 @@ let rec e_search n db_list local_db lg =
 	     (assumption_tac_list id)
 	     (e_search n db_list local_db)
 	     gls)
-	(ids_of_sign (pf_untyped_hyps g)) 
+	(pf_ids_of_hyps g)
     in
     let intro_tac = 
       apply_tac_list
 	(tclTHEN Tactics.intro 
 	   (fun g' -> 		   
-	      let (hid,htyp) = hd_sign (pf_untyped_hyps g') in
-	      let hintl = make_resolve_hyp hid htyp in
+	      let hintl = make_resolve_hyp (pf_last_hyp g') in
 	      (tactic_list_tactic 
 		 (e_search n db_list
 		    (Hint_db.add_list hintl local_db))) g')) 
@@ -249,7 +248,7 @@ let rec e_search n db_list local_db lg =
 
 let e_search_auto n db_list gl = 
   tactic_list_tactic 
-    (e_search n db_list (make_local_hint_db (pf_untyped_hyps gl)))
+    (e_search n db_list (make_local_hint_db (pf_hyps gl)))
     gl
 
 let eauto n dbnames = 
@@ -268,7 +267,7 @@ let full_eauto n gl =
   let dbnames = stringmap_dom !searchtable in
   let dbnames =  list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
-  let local_db = make_local_hint_db (pf_untyped_hyps gl) in
+  let local_db = make_local_hint_db (pf_hyps gl) in
   tclTRY (tclCOMPLETE (e_search_auto n db_list)) gl
 
 let default_full_auto gl = full_auto !default_search_depth gl
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 22bc94b691..ae5bed6741 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -47,10 +47,12 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
         let hdcncls = string_head hdcncl in 
         let elim =
 	  if lft2rgt then
-            pf_global gl (id_of_string 
-			    (hdcncls^(suff gl (pf_concl gl))^"_r"))
+            pf_global gl
+	      (id_of_string 
+		 (hdcncls^(Declare.elimination_suffix (sort_of_goal gl))^"_r"))
           else
-	    pf_global gl (id_of_string (hdcncls^(suff gl (pf_concl gl))))
+	    pf_global gl
+	      (id_of_string (hdcncls^(Declare.elimination_suffix (sort_of_goal gl))))
         in 
 	tclNOTSAMEGOAL (general_elim (c,l) (elim,[])) gl
    (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal 
@@ -445,8 +447,8 @@ let discriminable env sigma t1 t2 =
 
    the continuation then constructs the case-split.
  *)
-let push_rel_type sigma (na,t) env =
-  push_rel (na,make_typed t (get_sort_of env sigma t)) env
+let push_rel_type sigma (na,c,t) env =
+  push_rel (na,c,t) env
 
 let push_rels vars env =
   List.fold_right (fun nvar env -> push_rel_type Evd.empty nvar env) vars env
@@ -466,7 +468,7 @@ let descend_then sigma env head dirn =
       let p = lam_it (lift (mis_nrealargs mispec) resty) aritysign in
       let build_branch i =
 	let result = if i = dirn then dirnval else dfltval in
-	it_lambda_name env result cstr.(i-1).cs_args
+	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args
       in
       mkMutCase (make_default_case_info mispec) p head 
 	(List.map build_branch (interval 1 (mis_nconstr mispec)))))
@@ -510,7 +512,7 @@ let construct_discriminator sigma env dirn c sort =
   let cstrs = get_constructors indf in
   let build_branch i =
     let endpt = if i = dirn then true_0 else false_0 in
-    lam_it endpt cstrs.(i-1).cs_args 
+    it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args 
   in
   let build_match =
     mkMutCase (make_default_case_info mispec) p c 
@@ -608,7 +610,7 @@ let discr id gls =
      | Inl(cpath,MutConstruct(_,dirn),_) ->
 	 let e = pf_get_new_id (id_of_string "ee") gls in
 	 let e_env =
-	   push_var (e,assumption_of_judgment env sigma tj) env
+	   push_var_decl (e,assumption_of_judgment env sigma tj) env
 	 in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (VAR e) sort cpath in
@@ -714,7 +716,7 @@ let make_tuple env sigma (rterm,rty) lind =
     let a = type_of env sigma (Rel lind) in
     (* We replace (Rel lind) by (Rel 1) in rty then abstract on (na:a) *)
     let rty' = substnl [Rel 1] lind rty in
-    let na = fst (lookup_rel lind env) in
+    let na = fst (lookup_rel_type lind env) in
     let p = mkLambda na a rty' in
     (applist(exist_term,[a;p;(Rel lind);rterm]),
      applist(sig_term,[a;p]))
@@ -888,7 +890,7 @@ let inj id gls =
     | Inr posns ->
 	let e = pf_get_new_id (id_of_string "e") gls in
 	let e_env =
-	  push_var (e,assumption_of_judgment env sigma tj) env
+	  push_var_decl (e,assumption_of_judgment env sigma tj) env
 	in
 	let injectors =
 	  map_succeed
@@ -954,7 +956,7 @@ let decompEqThen ntac id gls =
      | Inl(cpath,MutConstruct(_,dirn),_) ->
 	 let e = pf_get_new_id (id_of_string "e") gls in
 	 let e_env =
-	   push_var (e,assumption_of_judgment env sigma tj) env in
+	   push_var_decl (e,assumption_of_judgment env sigma tj) env in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (VAR e) sort cpath in
 	 let (pf, absurd_term) =
@@ -966,7 +968,7 @@ let decompEqThen ntac id gls =
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
 	  let e_env =
-	    push_var (e,assumption_of_judgment env sigma tj) env in
+	    push_var_decl (e,assumption_of_judgment env sigma tj) env in
 	  let injectors =
 	    map_succeed
 	      (fun (cpath,t1_0,t2_0) ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 385cd574cd..39254ace08 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -66,16 +66,9 @@ let dest_match_eq gls eqn =
     
 let implicit = Sort implicit_sort
 
-let change_sign env (vars,rels) =
-  let env' = change_hyps (fun _ -> vars) env in
-  List.fold_left 
-    (fun env (n,t) -> 
-       let tt = execute_type env Evd.empty t in push_rel (n,tt) env)
-    env' rels
-
 (* Environment management *)
 let push_rel_type sigma (na,t) env =
-  push_rel (na,make_typed t (get_sort_of env sigma t)) env
+  push_rel_decl (na,make_typed t (get_sort_of env sigma t)) env
 
 let push_rels vars env =
   List.fold_left (fun env nvar -> push_rel_type Evd.empty nvar env) env vars
@@ -111,7 +104,7 @@ let make_inv_predicate env sigma ind id status concl =
 		let p = make_arity env true indf sort in
 		abstract_list_all env sigma p concl (realargs@[VAR id])
 	  in
-	  let hyps,_ = decompose_lam pred in
+	  let hyps,_ = decompose_lam_n (nrealargs+1) pred in
 	  let c3 = whd_beta (applist (pred,rel_list nrealargs (nrealargs +1))) 
 	  in
 	  (hyps,c3)
@@ -210,7 +203,7 @@ let generalizeRewriteIntros tac depids id gls =
 
 let var_occurs_in_pf gl id =
   occur_var id (pf_concl gl) or
-  exists_sign (fun _ t -> occur_var id t) (pf_untyped_hyps gl)
+  List.exists (fun (_,t) -> occur_var id t) (pf_hyps_types gl)
 
 let split_dep_and_nodep idl gl =
   (List.filter (var_occurs_in_pf gl) idl,
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 60a4cd3647..9e4386f1d6 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -28,9 +28,9 @@ open Inv
 
 let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments"
 
-let no_inductive_inconstr ass constr =
+let no_inductive_inconstr env constr =
   [< 'sTR "Cannot recognize an inductive predicate in "; 
-     prterm_env (Environ.context ass) constr;
+     prterm_env env constr;
      'sTR "."; 'sPC; 'sTR "If there is one, may be the structure of the arity";
      'sPC; 'sTR "or of the type of constructors"; 'sPC;
      'sTR "is hidden by constant definitions." >]
@@ -80,16 +80,18 @@ let no_inductive_inconstr ass constr =
  
 let thin_ids (hyps,vars) =
   fst
-    (it_sign
-       (fun ((ids,globs) as sofar) id a ->
+    (List.fold_left
+       (fun ((ids,globs) as sofar) (id,c,a) ->
           if List.mem id globs then
-            (id::ids,(global_vars a)@globs)
+	    match c with
+	      | None -> (id::ids,(global_vars a)@globs)
+	      | Some body -> (id::ids,(global_vars body)@(global_vars a)@globs)
           else sofar)
        ([],vars) hyps)
 
 (* returns the sub_signature of sign corresponding to those identifiers that
  * are not global. *)
-
+(*
 let get_local_sign sign =
   let lid = ids_of_sign sign in
   let globsign = Global.var_context() in
@@ -100,13 +102,13 @@ let get_local_sign sign =
       res_sign
   in 
   List.fold_right add_local lid nil_sign
-
+*)
 (* returs the identifier of lid that was the latest declared in sign.
  * (i.e. is the identifier id of lid such that 
  * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) >
  * for any id'<>id in lid).
  * it returns both the pair (id,(sign_prefix id sign)) *)
-
+(*
 let max_prefix_sign lid sign =
   let rec max_rec (resid,prefix) = function
     | [] -> (resid,prefix)
@@ -120,14 +122,14 @@ let max_prefix_sign lid sign =
   match lid with 
     | [] -> nil_sign
     | id::l -> snd (max_rec (id, sign_prefix id sign) l)
-
+*)
 let rec add_prods_sign env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
     | IsProd (na,c1,b) ->
 	let id = Environ.id_of_name_using_hdchar env t na in
 	let b'= subst1 (VAR id) b in
-	let j = make_typed c1 (Retyping.get_sort_of env sigma c1) in
-        add_prods_sign (Environ.push_var (id,j) env) sigma b'
+	let j = Retyping.get_assumption_of env sigma c1 in
+        add_prods_sign (Environ.push_var_decl (id,j) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates wether the inversion lemma is dependent or not.
@@ -145,7 +147,7 @@ let rec add_prods_sign env sigma t =
 
 let compute_first_inversion_scheme env sigma ind sort dep_option =
   let indf,realargs = dest_ind_type ind in
-  let allvars = ids_of_sign (var_context env) in
+  let allvars = ids_of_context env in
   let p = next_ident_away (id_of_string "P") allvars in
   let pty,goal =
     if dep_option  then
@@ -158,20 +160,18 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let i = mkAppliedInd ind in
       let ivars = global_vars i in
       let revargs,ownsign =
-	sign_it
-	  (fun id a (revargs,hyps) ->
-             if List.mem id ivars then
-	       ((VAR id)::revargs,(Name id,body_of_type a)::hyps)
+	fold_var_context
+	  (fun env (id,_,_ as d) (revargs,hyps) ->
+             if List.mem id ivars then ((VAR id)::revargs,add_var d hyps)
 	     else (revargs,hyps))
-          (var_context env) ([],[])
-      in 
-      let pty = it_prod_name env (mkSort sort) ownsign in
+          env ([],[]) in
+      let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
       let goal = mkArrow i (applist(VAR p, List.rev revargs)) in
       (pty,goal)
   in
   let npty = nf_betadeltaiota env sigma pty in
   let nptyj = make_typed npty (Retyping.get_sort_of env sigma npty) in
-  let extenv = push_var (p,nptyj) env in
+  let extenv = push_var_decl (p,nptyj) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
@@ -189,7 +189,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) in
   let (invEnv,invGoal) =
     compute_first_inversion_scheme env sigma ind sort dep_option in
-  assert (list_subset (global_vars invGoal)(ids_of_sign (var_context invEnv)));
+  assert (list_subset (global_vars invGoal) (ids_of_var_context (var_context invEnv)));
 (*
     errorlabstrm "lemma_inversion"
       [< 'sTR"Computed inversion goal was not closed in initial signature" >];
@@ -198,24 +198,23 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let pfs =
     solve_pftreestate (tclTHEN intro 
 			 (onLastHyp (compose inv_op out_some))) pfs in
-  let pf = proof_of_pftreestate pfs in
-  let (pfterm,meta_types) = 
-    Refiner.extract_open_proof (var_context pf.goal.evar_env) pf in
+  let (pfterm,meta_types) = extract_open_pftreestate pfs in
+  let global_var_context = Global.var_context () in
   let ownSign =
-    sign_it
-      (fun id ty sign ->
-         if mem_sign (Global.var_context()) id then sign
-         else ((Name id,body_of_type ty)::sign))
-      (var_context invEnv) [] in
+    fold_var_context
+      (fun env (id,_,_ as d) sign ->
+         if mem_var_context id global_var_context then sign
+	 else add_var d sign)
+      invEnv empty_var_context in
   let (_,ownSign,mvb) =
     List.fold_left
       (fun (avoid,sign,mvb) (mv,mvty) ->
          let h = next_ident_away (id_of_string "H") avoid in
-	 (h::avoid, (Name h,mvty)::sign, (mv,VAR h)::mvb))
-      (ids_of_sign (var_context invEnv), ownSign, [])
+	 (h::avoid, add_var_decl (h,mvty) sign, (mv,VAR h)::mvb))
+      (ids_of_context invEnv, ownSign, [])
       meta_types in
   let invProof = 
-    it_lambda_name env (local_strong (whd_meta mvb) pfterm) ownSign in
+    it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign in
   invProof
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
@@ -232,8 +231,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
 let inversion_lemma_from_goal n na id sort dep_option inv_op =
   let pts = get_pftreestate() in
   let gl = nth_goal_of_pftreestate n pts in
-  let hyps = pf_untyped_hyps gl in
-  let t = snd (lookup_sign id hyps) in
+  let t = pf_get_hyp_typ gl id in
   let env = pf_env gl and sigma = project gl in
   let fv = global_vars t in
 (* Pourquoi ??? 
@@ -329,7 +327,7 @@ let lemInv id c gls =
     |  UserError (a,b) -> 
 	 errorlabstrm "LemInv" 
 	   [< 'sTR "Cannot refine current goal with the lemma "; 
-	      prterm_env (Global.context()) c  >] 
+	      prterm_env (Global.env()) c  >] 
 
 let useInversionLemma =
   let gentac =
diff --git a/tactics/refine.ml b/tactics/refine.ml
index f953d349ef..8a43cff935 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -120,7 +120,7 @@ let replace_in_array env a =
     
 let fresh env n =
   let id = match n with Name x -> x | _ -> id_of_string "_" in
-  next_global_ident_away id (ids_of_sign (var_context env))
+  next_global_ident_away id (ids_of_var_context (var_context env))
 
 let rec compute_metamap env = function
   (* le terme est directement une preuve *)
@@ -140,8 +140,8 @@ let rec compute_metamap env = function
   | DOP2(Lambda,c1,DLAM(name,c2)) as c ->
       let v = fresh env name in
       (** let tj = ise_resolve_type true empty_evd [] (gLOB sign) c1 in **)
-      let tj = execute_type env Evd.empty c1 in
-      let env' = push_var (v,tj) env in
+      let tj = Retyping.get_assumption_of env Evd.empty c1 in
+      let env' = push_var_decl (v,tj) env in
       begin match compute_metamap env' (subst1 (VAR v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
@@ -167,7 +167,7 @@ let rec compute_metamap env = function
       let vi = List.rev (List.map (fresh env) fi) in
       let env' =
 	List.fold_left
-	  (fun env (v,ar) -> push_var (v,execute_type env Evd.empty ar) env)
+	  (fun env (v,ar) -> push_var_decl (v,Retyping.get_assumption_of env Evd.empty ar) env)
 	  env
 	  (List.combine vi (Array.to_list ai)) 
       in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6d9aca72c6..a37a395dd2 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -52,7 +52,7 @@ let tclMAP tacfun l =
 (* apply a tactic to the nth element of the signature  *)
 
 let tclNTH_HYP m (tac : constr->tactic) gl =
-  tac (try VAR(fst(nth_sign (pf_untyped_hyps gl) m)) 
+  tac (try VAR(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) 
        with Failure _ -> error "No such assumption") gl
 
 (* apply a tactic to the last element of the signature  *)
@@ -65,10 +65,10 @@ let tclTRY_sign (tac : constr->tactic) sign gl =
     | [s]     -> tac (VAR(s)) (* added in order to get useful error messages *)
     | (s::sl) -> tclORELSE (tac (VAR(s))) (arec sl) 
   in 
-  arec (ids_of_sign sign) gl
+  arec (ids_of_var_context sign) gl
 
 let tclTRY_HYPS (tac : constr->tactic) gl = 
-  tclTRY_sign tac (pf_untyped_hyps gl) gl
+  tclTRY_sign tac (pf_hyps gl) gl
 
 (* OR-branch *)
 let tryClauses tac = 
@@ -101,10 +101,10 @@ let nth_clause n gl =
   if n = 0 then 
     None
   else if n < 0 then 
-    let id = List.nth (ids_of_sign (pf_untyped_hyps gl)) (-n-1) in 
+    let id = List.nth (pf_ids_of_hyps gl) (-n-1) in 
     Some id
   else 
-    let id = List.nth (ids_of_sign (pf_untyped_hyps gl)) (n-1) in 
+    let id = List.nth (pf_ids_of_hyps gl) (n-1) in 
     Some id
 
 (* Gets the conclusion or the type of a given hypothesis *)
@@ -112,7 +112,7 @@ let nth_clause n gl =
 let clause_type cls gl =
   match cls with
     | None    -> pf_concl gl
-    | Some id -> pf_get_hyp gl id
+    | Some id -> pf_get_hyp_typ gl id
 
 (* Functions concerning matching of clausal environments *)
 
@@ -132,7 +132,7 @@ let onCL cfind cltac gl = cltac (cfind gl) gl
 
 (* Create a clause list with all the hypotheses from the context *)
 
-let allHyps gl = (List.map in_some (ids_of_sign (pf_untyped_hyps gl)))
+let allHyps gl = List.map in_some (pf_ids_of_hyps gl)
 
 
 (* Create a clause list with all the hypotheses from the context, occuring
@@ -140,20 +140,19 @@ let allHyps gl = (List.map in_some (ids_of_sign (pf_untyped_hyps gl)))
 
 let afterHyp id gl =
   List.map in_some
-    (fst (list_splitby (fun hyp -> hyp = id) 
-	    (ids_of_sign (pf_untyped_hyps gl))))
+    (fst (list_splitby (fun hyp -> hyp = id) (pf_ids_of_hyps gl)))
     
 
 (* Create a singleton clause list with the last hypothesis from then context *)
 
 let lastHyp gl = 
-  let (id,_) = hd_sign (pf_untyped_hyps gl) in [(Some id)]
+  let id = List.hd (pf_ids_of_hyps gl) in [(Some id)]
 
 (* Create a clause list with the n last hypothesis from then context *)
 
 let nLastHyps n gl =
   let ids =
-    try list_firstn n (ids_of_sign (pf_untyped_hyps gl))
+    try list_firstn n (pf_ids_of_hyps gl)
     with Failure "firstn" -> error "Not enough hypotheses in the goal"
   in 
   List.map in_some ids
@@ -162,7 +161,7 @@ let nLastHyps n gl =
 (* A clause list with the conclusion and all the hypotheses *)
 
 let allClauses gl = 
-  let ids = ids_of_sign(pf_untyped_hyps gl) in  
+  let ids = pf_ids_of_hyps gl in  
   (None::(List.map in_some ids))
 
 let onClause t cls gl  = t cls gl
@@ -193,7 +192,7 @@ let conclPattern concl pat tacast gl =
   let ast_bindings = 
     List.map 
       (fun (i,c) ->
-	 (i, Termast.ast_of_constr false (assumptions_for_print []) c))
+	 (i, Termast.ast_of_constr false (pf_env gl) c))
       constr_bindings in 
   let tacast' = Coqast.subst_meta ast_bindings tacast in
   Tacinterp.interp tacast' gl
@@ -285,21 +284,6 @@ let sort_of_goal gl =
 (* Find the right elimination suffix corresponding to the sort of the goal *)
 (* c should be of type A1->.. An->B with B an inductive definition *)
 
-let suff gl cl = match hnf_type_of gl cl with
-  | DOP0(Sort(Type(_)))    -> "_rect"
-  | DOP0(Sort(Prop(Null))) -> "_ind"
-  | DOP0(Sort(Prop(Pos)))  -> "_rec"
-  | _                      -> anomaly "goal should be a type"
-
-(* Look up function for the default elimination constant *)
-
-let lookup_eliminator sign path suff =
-  let name = id_of_string ((string_of_id (basename path)) ^ suff) in
-  try 
-    Declare.global_reference (kind_of_path path) name
-  with UserError _ -> 
-    VAR(fst(lookup_glob name (gLOB sign)))
-
 let last_arg = function
   | DOPN(AppL,cl) -> cl.(Array.length cl - 1)
   | _ -> anomaly "last_arg"
@@ -355,9 +339,7 @@ let general_elim_then_using
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
   let (ity,path_name,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
-  let elim = 
-    lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl))
-  in
+  let elim = lookup_eliminator (pf_env gl) path_name (sort_of_goal gl) in
   general_elim_then_using
     elim elim_sign tac predicate (indbindings,elimbindings) c gl
 
@@ -409,7 +391,7 @@ let make_elim_branch_assumptions ba gl =
       | (_, _) -> error "make_elim_branch_assumptions"
   in 
   makerec ([],[],[],[],[]) ba.branchsign
-    (try list_firstn ba.nassums (ids_of_sign (pf_untyped_hyps gl))
+    (try list_firstn ba.nassums (pf_ids_of_hyps gl)
      with Failure _ -> anomaly "make_elim_branch_assumptions")
 
 let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
@@ -437,7 +419,7 @@ let make_case_branch_assumptions ba gl =
       | (_, _) -> error "make_case_branch_assumptions"
   in 
   makerec ([],[],[],[]) ba.branchsign
-    (try list_firstn ba.nassums (ids_of_sign (pf_untyped_hyps gl))
+    (try list_firstn ba.nassums (pf_ids_of_hyps gl)
      with Failure _ -> anomaly "make_case_branch_assumptions")
 
 let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 056ac353f2..0cdedd8c68 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -34,7 +34,7 @@ val tclWEAK_PROGRESS : tactic -> tactic
 val tclNTH_HYP       : int -> (constr -> tactic) -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 val tclLAST_HYP      : (constr -> tactic) -> tactic
-val tclTRY_sign      : (constr -> tactic) -> constr signature -> tactic
+val tclTRY_sign      : (constr -> tactic) -> var_context -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
 
 (*val dyn_tclIDTAC     : tactic_arg list -> tactic
@@ -103,9 +103,7 @@ type branch_assumptions = {
   indargs   : identifier list} (* the inductive arguments *)
 
 val sort_of_goal      : goal sigma -> sorts
-val suff              : goal sigma -> constr -> string
-val lookup_eliminator : 
-  typed_type signature -> section_path -> string -> constr
+(*val suff              : goal sigma -> constr -> string*)
 
 val general_elim_then_using :
   constr ->  (inductive -> int -> bool list) -> 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9a03eca979..0beab3f7a1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -11,6 +11,7 @@ open Term
 open Inductive
 open Reduction
 open Environ
+open Declare
 open Evd
 open Pfedit
 open Tacred
@@ -153,7 +154,7 @@ let reduct_in_concl redfun gl =
   convert_concl (pf_reduce redfun gl (pf_concl gl)) gl
     
 let reduct_in_hyp redfun id gl  = 
-  let ty = pf_get_hyp gl id in
+  let ty = pf_get_hyp_typ gl id in
   let redfun' = under_casts (fun _ _ -> pf_reduce redfun gl) in
   convert_hyp id (redfun' (pf_env gl) (project gl) ty) gl
     
@@ -261,7 +262,7 @@ let next_global_ident_away id avoid =
     next_global_ident_from (lift_ident id) avoid
 
 let fresh_id avoid id gl =
-  next_global_ident_away id (avoid@(ids_of_sign (pf_untyped_hyps gl)))
+  next_global_ident_away id (avoid@(pf_ids_of_hyps gl))
     
 let id_of_name_with_default s = function
   | Anonymous -> id_of_string s
@@ -407,23 +408,33 @@ let rec intros_move = function
       tclTHEN (central_intro (IMustBe hyp) destopt false)
 	(intros_move rest)
 
+let occur_var_in_decl id (c,t) = 
+  match c with
+    | None -> occur_var id (body_of_type t)
+    | Some body -> occur_var id body || occur_var id (body_of_type t)
+
+let dependent_in_decl a (c,t) =
+  match c with
+    | None -> dependent a (body_of_type t)
+    | Some body -> dependent a body || dependent a (body_of_type t)
+
 let move_to_rhyp rhyp gl =
-  let rec get_lhyp lastfixed deptyp = function
+  let rec get_lhyp lastfixed depdecls = function
     | [] ->
 	(match rhyp with
 	   | None -> lastfixed
       	   | Some h -> anomaly ("Hypothesis should occur: "^ (string_of_id h)))
-    | (hyp,typ) as ht :: rest ->
+    | (hyp,c,typ) as ht :: rest ->
 	if Some hyp = rhyp then 
 	  lastfixed
-	else if List.exists (occur_var hyp) deptyp then 
-	  get_lhyp lastfixed (typ::deptyp) rest
+	else if List.exists (occur_var_in_decl hyp) depdecls then 
+	  get_lhyp lastfixed ((c,typ)::depdecls) rest
         else 
-	  get_lhyp (Some hyp) deptyp rest
+	  get_lhyp (Some hyp) depdecls rest
   in
-  let sign = pf_untyped_hyps gl in
-  let (hyp,typ) = hd_sign sign in
-  match get_lhyp None [typ] (list_of_sign sign) with
+  let sign = pf_hyps gl in
+  let (hyp,c,typ) = List.hd sign in
+  match get_lhyp None [c,typ] sign with
     | None -> tclIDTAC gl
     | Some hypto -> move_hyp true hyp hypto gl
 
@@ -585,25 +596,30 @@ let generalize_goal gl c cl =
 	  prod_name (Global.env()) (Anonymous, t, cl')
 
 let generalize_dep c gl =
-  let sign = pf_untyped_hyps gl in
-  let init_ids = ids_of_sign (Global.var_context()) in
-  let rec seek ((hl,tl) as toquant) h t =
-    if List.exists (fun id -> occur_var id t) hl or dependent c t then 
-      (h::hl,t::tl)
+  let sign = pf_hyps gl in
+  let init_ids = ids_of_var_context (Global.var_context()) in
+  let rec seek toquant (h,body,t as d) =
+    if List.exists (fun (id,_,_) -> occur_var_in_decl id (body,t)) toquant
+      or dependent_in_decl c (body,t) then 
+      d::toquant
     else 
       toquant
   in
-  let (hl,tl) = it_sign seek ([],[]) sign in
-  let tothin = List.filter (fun id -> not (List.mem id init_ids)) hl in
+  let to_quantify = List.fold_left seek [] sign in
+  let qhyps = List.map (fun (id,_,_) -> id) to_quantify in
+  let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
   let tothin' =
     match c with
-      | VAR id when mem_sign sign id & not (List.mem id init_ids) -> id::tothin
+      | VAR id when mem_var_context id sign & not (List.mem id init_ids)
+	  -> id::tothin
       | _ -> tothin
   in
-  let cl' = List.fold_right2 mkNamedProd hl tl (pf_concl gl) in
+  let cl' =
+    List.fold_left 
+      (fun c d -> mkNamedProd_or_LetIn d c) (pf_concl gl) to_quantify in
   let cl'' = generalize_goal gl c cl' in
   tclTHEN
-    (apply_type cl'' (c::(List.map (fun id -> VAR id) hl)))
+    (apply_type cl'' (c::(List.map (fun id -> VAR id) qhyps)))
     (thin (List.rev tothin'))
     gl
     
@@ -630,30 +646,42 @@ let quantify lconstr =
    tclIDTAC
 *)
 
-(* A dependent cut rule à la sequent calculus *) 
+(* A dependent cut rule à la sequent calculus
+   ------------------------------------------
+   Sera simplifiable le jour où il y aura un let in primitif dans constr
 
-(* Sera simplifiable le jour où il y aura un let in primitif dans constr *) 
+   [letin_tac b na c occ_ccl occ_hyps gl] transforms
+   [...x1:T1(c),...,x2:T2(c),... |- G(c)] into
+   [...x:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or
+   [...x:T;H:x=c;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true
 
-(* if [occhypl] is empty, [c] is substituted in every hyp where it occurs   *)
-(* if name = Anonymous, the name is build from the first letter of the type *)
+   [occ_hyps] and [occ_ccl] tells which occurrences of [c] have to be substd;
+   if [occ_hyps] is empty, [c] is substituted in every hyp where it occurs;
+   if name = Anonymous, the name is build from the first letter of the type;
 
-let letin_abstract id c occ_ccl occhypl gl =
-  let allhyp = occhypl=[] in
-  let hyps = pf_untyped_hyps gl in
-  let abstract ((dephyps,deptyps,marks,occl as accu),lhyp) hyp typ =
+   The tactic first quantify the goal over x1, x2,... then substitute then
+   re-intro x1, x2,... at their initial place ([marks] is internally
+   used to remember the place of x1, x2, ...: it is the list of hypotheses on
+   the left of each x1, ...).
+*)
+(*
+let letin_abstract id c occ_ccl occ_hyps gl =
+  let allhyp = occ_hyps=[] in
+  let hyps = pf_hyps gl in
+  let abstract ((depdecls,marks,occl as accu),lhyp) (hyp,bodyopt,typ as d) =
     try 
       let occ = if allhyp then [] else List.assoc hyp occl in
-      let newtyp = subst1 (VAR id) (subst_term_occ occ c typ) in
+      let newdecl = subst1 (VAR id) (subst_term_occ_decl occ c d) in
       let newoccl = list_except_assoc hyp occl in
-      if typ=newtyp then 
+      if d=newdecl then
 	(accu,Some hyp)
       else 
-	((hyp::dephyps,newtyp::deptyps,(hyp,lhyp)::marks,newoccl),lhyp)
+	((newdecl::depdecls,(hyp,lhyp)::marks,newoccl),lhyp)
     with Not_found -> 
       (accu,Some hyp) 
   in
-  let (dephyps,deptyps,marks,rest),_ =
-    it_sign abstract (([],[],[],occhypl),None) hyps in
+  let (depdecls,marks,rest),_ =
+    it_sign abstract (([],[],[],occ_hyps),None) hyps in
   if rest <> [] then begin
     let id = fst (List.hd rest) in
     if mem_sign hyps id
@@ -664,14 +692,14 @@ let letin_abstract id c occ_ccl occhypl gl =
     | None -> (pf_concl gl)
     | Some occ -> subst1 (VAR id) (subst_term_occ occ c (pf_concl gl)) 
   in
-  (dephyps,deptyps,marks,ccl)
+  (depdecls,marks,ccl)
 
-let letin_tac with_eq name c occ_ccl occhypl gl =
+let letin_tac with_eq name c occ_ccl occ_hyps gl =
   let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
   let hyps = pf_untyped_hyps gl in
   let id = next_global_ident_away x (ids_of_sign hyps) in
   if mem_sign hyps id then error "New variable is already declared";
-  let (dephyps,deptyps,marks,ccl)= letin_abstract id c occ_ccl occhypl gl in 
+  let (depdecls,marks,ccl)= letin_abstract id c occ_ccl occ_hyps gl in 
   let t = pf_type_of gl c in
   let (eqc,reflc) =
     let sort = pf_type_of gl t in
@@ -682,8 +710,8 @@ let letin_tac with_eq name c occ_ccl occhypl gl =
     else error "Not possible with proofs yet" 
   in
   let heq = next_global_ident_away (id_of_string "Heq") (ids_of_sign hyps) in
-  let tmpcl = List.fold_right2 mkNamedProd dephyps deptyps ccl in
-  let tmpargs = List.map (fun id -> VAR id) dephyps in
+  let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
+  let tmpargs = List.map (fun (id,_,_) -> VAR id) depdecls in
   let newcl,args =
     if with_eq then
       let eq = applist (eqc,[t;VAR id;c]) in
@@ -706,7 +734,8 @@ let dyn_lettac args gl = match args with
   | [Identifier id; Constr c; Letpatterns (o,l)]    ->
       letin_tac true (Name id) c o l gl
   | l -> bad_tactic_args "letin" l
-
+*)
+let dyn_lettac a = failwith "TO REDO"
 
 (********************************************************************)
 (*               Exact tactics                                      *)
@@ -738,13 +767,13 @@ let dyn_exact cc gl = match cc with
 
 let (assumption : tactic) = fun gl ->
   let concl =  pf_concl gl in 
-  let rec arec sign =
-    if isnull_sign sign then error "No such assumption";
-    let (s,a) = hd_sign sign in
-    if pf_conv_x_leq gl a concl then refine (VAR(s)) gl
-    else arec (tl_sign sign)
+  let rec arec = function
+    | [] -> error "No such assumption"
+    | (id,c,t)::rest -> 
+	if pf_conv_x_leq gl (body_of_type t) concl then refine (VAR id) gl
+	else arec rest
   in
-  arec (pf_untyped_hyps gl)
+  arec (pf_hyps gl)
 
 let dyn_assumption = function
   | [] -> assumption
@@ -966,9 +995,7 @@ let general_elim (c,lbindc) (elimc,lbindelimc) gl =
 let default_elim (c,lbindc)  gl = 
   let (path_name,_,t) = reduce_to_ind (pf_env gl) (project gl) 
 			  (pf_type_of gl c) in
-  let elimc =
-    lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl))
-  in  
+  let elimc = lookup_eliminator (pf_env gl) path_name (sort_of_goal gl) in  
   general_elim (c,lbindc) (elimc,[]) gl
 
 
@@ -1019,8 +1046,8 @@ let rec is_rec_arg indpath t =
 let induct_discharge indpath statuslists cname destopt avoid (_,t) =
   let (lstatus,rstatus) = statuslists in
   let tophyp = ref None in
-  let (l,_) = decompose_prod t in
-  let n = List.length (List.filter (fun (_,t') -> is_rec_arg indpath t') l) in
+  let (l,_) = decompose_prod_assum t in
+  let n = List.length (List.filter (fun (_,_,t') -> is_rec_arg indpath (body_of_type t')) l) in
   let recvarname =
     if n=1 then 
       cname
@@ -1057,14 +1084,9 @@ let induct_discharge indpath statuslists cname destopt avoid (_,t) =
      substitutions aussi sur l'argument voisin *)
 
 (* Marche pas... faut prendre en compte l'occurence précise... *)
-
+(*
 let atomize_param_of_ind hyp0 gl =
-  let tmptyp0 =
-    try 
-      (snd(lookup_sign hyp0 (pf_untyped_hyps gl)))
-    with Not_found -> 
-      error ("No such hypothesis : " ^ (string_of_id hyp0)) 
-  in
+  let tmptyp0 = pf_get_hyp_typ gl hyp0 in
   let (mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in
   let mis = Global.lookup_mind_specif mind in
   let nparams = mis_nparams mis in
@@ -1073,7 +1095,7 @@ let atomize_param_of_ind hyp0 gl =
   (* le gl est important pour ne pas préévaluer *)
   let rec atomize_one i avoid gl =
     if i<>nparams then 
-      let tmptyp0 = pf_get_hyp gl hyp0 in
+      let tmptyp0 = pf_get_hyp_typ gl hyp0 in
       let (_,indtyp,_) = pf_reduce_to_mind gl tmptyp0 in
       match (destAppL (whd_castapp indtyp)).(i) with
 	| VAR id when not (List.exists (occur_var id) avoid) ->
@@ -1309,7 +1331,7 @@ let new_induct c gl =
 	tclTHEN
 	  (letin_tac true (Name id) c (Some []) [])
 	  (induction_with_atomization_of_ind_arg id) gl
-	  
+*)
 (***)
 
 (* The registered tactic, which calls the default elimination
@@ -1330,10 +1352,14 @@ let dyn_elim = function
   | l -> bad_tactic_args "elim" l
 	
 (* Induction tactics *)
-
+(*
 let induct s =
   tclORELSE (tclTHEN (intros_until s) (tclLAST_HYP simplest_elim))
     (induction_from_context s)
+*)
+let induct s =
+  tclTHEN (intros_until s) (tclLAST_HYP simplest_elim)
+
 
 let induct_nodep n = tclTHEN (intros_do n) (tclLAST_HYP simplest_elim)
 
@@ -1398,9 +1424,7 @@ let elim_scheme_type elim t gl =
 
 let elim_type t gl =
   let (path_name,tind,t) = reduce_to_ind (pf_env gl) (project gl) t in
-  let elimc =
-    lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl))
-  in 
+  let elimc = lookup_eliminator (pf_env gl) path_name (sort_of_goal gl) in
   match t with 
     | DOP2(Prod,_,_) -> error "Not an inductive definition"
     | _              -> elim_scheme_type elimc tind gl
@@ -1442,7 +1466,7 @@ let dyn_case_type = function
  *)
 
 let andE id gl =
-  let t = pf_get_hyp gl id in
+  let t = pf_get_hyp_typ gl id in
   if is_conjunction (pf_hnf_constr gl t) then 
     (tclTHEN (simplest_elim (VAR id)) (tclDO 2 intro)) gl
   else 
@@ -1455,7 +1479,7 @@ let dAnd cls gl =
     | Some id -> andE id  gl
 
 let orE id gl =
-  let t = pf_get_hyp gl id in
+  let t = pf_get_hyp_typ gl id in
   if is_disjunction (pf_hnf_constr gl t) then 
     (tclTHEN (simplest_elim (VAR id)) intro) gl
   else 
@@ -1468,7 +1492,7 @@ let dorE b cls gl =
     |  None     -> (if b then right else left) [] gl
 
 let impE id gl =
-  let t = pf_get_hyp gl id in
+  let t = pf_get_hyp_typ gl id in
   if is_imp_term (pf_hnf_constr gl t) then 
     let (dom, _, rng) = destProd (pf_hnf_constr gl t) in 
     (tclTHENS (cut_intro rng) 
@@ -1490,7 +1514,7 @@ let dImp cls gl =
 (* Contradiction *)
 
 let contradiction_on_hyp id gl =
-  let hyp = pf_get_hyp gl id in
+  let hyp = pf_get_hyp_typ gl id in
   if is_empty_type hyp then
     simplest_elim (VAR id) gl
   else 
@@ -1503,10 +1527,10 @@ let absurd c gls =
      (tclTHEN (elim_type falseterm) (cut c)) 
      ([(tclTHENS
           (cut (applist(pf_global gls (id_of_string "not"),[c]))) 
-	  ([(tclTHEN (intros)
+	  ([(tclTHEN intros
 	       ((fun gl ->
-		   let (ida,_) = pf_nth_hyp gl 1
-                   and (idna,_) = pf_nth_hyp gl 2 in
+		   let ida = pf_nth_hyp_id gl 1
+                   and idna = pf_nth_hyp_id gl 2 in
                    exact (applist(VAR idna,[VAR ida])) gl)));
             tclIDTAC]));
        tclIDTAC])) gls
@@ -1626,32 +1650,33 @@ let dyn_transitivity = function
 let abstract_subproof name tac gls = 
   let env = Global.env() in
   let current_sign = Global.var_context()
-  and global_sign = pf_untyped_hyps gls in
-  let sign = Sign.sign_it 
-               (fun id typ s -> 
-		  if mem_sign current_sign id then s else add_sign (id,typ) s) 
-               global_sign nil_sign 
+  and global_sign = pf_hyps gls in
+  let sign = List.fold_right
+               (fun (id,_,_ as d) s -> 
+		  if mem_var_context id current_sign then s else add_var d s) 
+               global_sign empty_var_context
   in
   let na = next_global_ident_away name
-             (ids_of_sign global_sign)  in 
-  let concl = Sign.it_sign (fun t id typ -> mkNamedProd id typ t)
+             (ids_of_var_context global_sign) in
+  let concl = List.fold_left (fun t d -> mkNamedProd_or_LetIn d t)
                 (pf_concl gls) sign in
   let env' = change_hyps (fun _ -> current_sign) env in
   let lemme =
     start_proof na Declare.NeverDischarge env' concl;
     let _,(const,strength) =
       try
-	by (tclCOMPLETE (tclTHEN (tclDO (sign_length sign) intro) tac)); 
-	release_proof ()
+	by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
+	let r = cook_proof () in 
+	delete_current_proof (); r
       with e when catchable_exception e -> 
-	(abort_current_proof(); raise e)
+	(delete_current_proof(); raise e)
     in   (* Faudrait un peu fonctionnaliser cela *)
     Declare.declare_constant na (const,strength);
     let newenv = Global.env() in
     Declare.construct_reference newenv CCI na
   in
   exact (applist (lemme,
-		  List.map (fun id -> VAR id) (List.rev (ids_of_sign sign))))
+		  List.map (fun id -> VAR id) (List.rev (ids_of_var_context sign))))
     gls
 
 let tclABSTRACT name_op tac gls = 
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 0130566b45..47f7a40cf9 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -23,17 +23,19 @@ open Proof_trees
 open Clenv
 open Pattern
 
+(* Faut-il comparer le corps des définitions de l'environnement ? *)
 let hlset_subset hls1 hls2 =
-  List.for_all (fun e -> List.exists (fun e' -> eq_constr e e') hls2) hls1
+  List.for_all
+    (fun (_,_,e) -> List.exists
+	 (fun (_,_,e') -> eq_constr (body_of_type e) (body_of_type e'))
+	 hls2)
+    hls1
 
 let hlset_eq hls1 hls2 =
   hlset_subset hls1 hls2 & hlset_subset hls2 hls1
   
 let eq_gls g1 g2 =
-    eq_constr (pf_concl g1) (pf_concl g2)
- &  (let hl1 = vals_of_sign (pf_untyped_hyps g1)
-     and hl2 = vals_of_sign (pf_untyped_hyps g2) in 
-     hlset_eq hl1 hl2)
+  eq_constr (pf_concl g1) (pf_concl g2) & hlset_eq (pf_hyps g1) (pf_hyps g2)
 
 let gls_memb bTS g = List.exists (eq_gls g) bTS
 
@@ -1715,14 +1717,13 @@ let rec lisvarprop = function
 (*-- Dado el ambiente COQ construye el lado izquierdo de un secuente
      (hipotesis) --*)
 let rec constr_lseq gls = function
-  | ([],[]) -> []
-  | (idx::idy,hx::hy) -> 
-      (match (pf_type_of gls hx) with
-         | DOP0 (Sort (Prop Null)) -> 
-             (TVar(string_of_id idx),tauto_of_cci_fmla gls hx)
-             :: constr_lseq gls (idy,hy)
-         |_-> constr_lseq gls (idy,hy))
-  | _ -> []
+  | [] -> []
+  | (idx,c,hx)::rest -> 
+      match Retyping.get_sort_of (pf_env gls) (project gls) (incast_type hx) with
+        | Prop Null -> 
+            (TVar(string_of_id idx),tauto_of_cci_fmla gls (body_of_type hx))
+            :: constr_lseq gls rest
+        |_-> constr_lseq gls rest
 
 (*-- Dado un estado COQ construye el lado derecho de un secuente
      (conclusion) --*)
@@ -1735,7 +1736,7 @@ let rec pos_lis x = function
   | a::r -> if (x=a) then 1 else 1 + (pos_lis x r) 
 
 (*-- Construye un termino constr dado una formula tauto --*)
-let rec cci_of_tauto_fml env = 
+let rec cci_of_tauto_fml () = 
   let cAnd = global_reference CCI (id_of_string "and") 
   and cOr =  global_reference CCI (id_of_string "or")  
   and cFalse = global_reference CCI (id_of_string "False") 
@@ -1743,13 +1744,13 @@ let rec cci_of_tauto_fml env =
   and cEq = global_reference CCI (id_of_string "eq") in
   function
     | FAnd(a,b) ->  applistc cAnd 
-                    [cci_of_tauto_fml env a;cci_of_tauto_fml env b]
+                    [cci_of_tauto_fml () a;cci_of_tauto_fml () b]
     | FOr(a,b)  ->  applistc cOr 
-                    [cci_of_tauto_fml env a; cci_of_tauto_fml env b]
+                    [cci_of_tauto_fml () a; cci_of_tauto_fml () b]
     | FEq(a,b,c)->  applistc cEq
-                    [cci_of_tauto_fml env a; cci_of_tauto_fml env b;
-                     cci_of_tauto_fml env c]
-    | FImp(a,b) ->  mkArrow (cci_of_tauto_fml env a) (cci_of_tauto_fml env b) 
+                    [cci_of_tauto_fml () a; cci_of_tauto_fml () b;
+                     cci_of_tauto_fml () c]
+    | FImp(a,b) ->  mkArrow (cci_of_tauto_fml () a) (cci_of_tauto_fml () b) 
     | FPred a   ->  a  
     | FFalse    ->  cFalse
     | FTrue     ->  cTrue
@@ -1761,10 +1762,11 @@ let rec cci_of_tauto_fml env =
 
 let search env id =
   try
-    (match lookup_id id (Environ.context env) with
-       | RELNAME (n,_) -> Rel n
-       | GLOBNAME _    -> VAR id)
+    Rel (fst (lookup_rel_id id (Environ.rel_context env)))
   with Not_found ->
+  if mem_var_context id (Environ.var_context env) then
+    VAR id
+  else
     global_reference CCI id
 
 (*-- Construye un termino constr de un termino tauto --*)
@@ -1786,37 +1788,37 @@ let cci_of_tauto_term env t =
                                    search env (id_of_string x))
                             with _ -> raise TacticFailure)
     | TZ(f,x)           -> applistc cFalse_ind
-          [cci_of_tauto_fml env f;ter_constr l x]
+          [cci_of_tauto_fml () f;ter_constr l x]
     | TSum(t1,t2)       -> ter_constr l t1 
     | TExi (x)          -> (try search env (id_of_string x) with
 				_ -> raise TacticFailure)
     | TApl(_,_,t1,t2)   -> applistc (ter_constr l t1) [ter_constr l t2]
     | TPar(f1,f2,t1,t2) -> applistc cconj
-          [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2;
+          [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2;
            ter_constr l t1;ter_constr l t2]
     | TInl(f1,f2,t)     -> applistc cor_introl
-          [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2;
+          [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2;
            ter_constr l t]
     | TInr(f1,f2,t)     -> applistc cor_intror
-          [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2;
+          [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2;
            ter_constr l t]
     | TFst(f1,f2,t)     -> applistc cproj1
-          [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2;
+          [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2;
            ter_constr l t]
     | TSnd(f1,f2,t)     -> applistc cproj2
-          [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2;
+          [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2;
            ter_constr l t]
     | TRefl(f1,f2)      -> applistc crefl
-          [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2]
+          [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2]
     | TSim(f1,f2,f3,t) -> applistc csim
-          [cci_of_tauto_fml env f1;cci_of_tauto_fml env f2;
-           cci_of_tauto_fml env f3;ter_constr l t]
+          [cci_of_tauto_fml () f1;cci_of_tauto_fml () f2;
+           cci_of_tauto_fml () f3;ter_constr l t]
     | TCase(lf,lt)      -> applistc cor_ind
-          ((List.map (cci_of_tauto_fml env) lf)@
+          ((List.map (cci_of_tauto_fml ()) lf)@
            (List.map (ter_constr l) lt))
     | TFun(n,f,t)       ->  
 	Environ.lambda_name env
-	  (Name(id_of_string n ), cci_of_tauto_fml env f,ter_constr (n::l) t)
+	  (Name(id_of_string n ), cci_of_tauto_fml () f,ter_constr (n::l) t)
     | TTrue             -> ci
     | TLis _            -> raise TacticFailure
     | TLister _         -> raise TacticFailure
@@ -1843,17 +1845,15 @@ let exacto tt gls =
     
 let subbuts l hyp = cut_in_parallelUsing
                       (lisvar l) 
-                      (List.map (cci_of_tauto_fml (gLOB hyp)) (lisfor l))
+                      (List.map (cci_of_tauto_fml ()) (lisfor l))
 
 let t_exacto = ref (TVar "#")
 
 let tautoOR ti gls =
-  let hyp = pf_untyped_hyps gls in
   let thyp = pf_hyps gls in
-  hipvar := ids_of_sign hyp; 
+  hipvar := ids_of_var_context thyp; 
   let but = pf_concl gls in
-  let seq = (constr_lseq gls (ids_of_sign hyp,vals_of_sign hyp),
-	     constr_rseq gls but) in 
+  let seq = (constr_lseq gls thyp, constr_rseq gls but) in 
   let vp = lisvarprop (ante seq) in
   match naive ti vp seq with
     | {arb=Nil} -> 
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 48ae03cc92..005be137e0 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -22,10 +22,10 @@ open Clenv
 type wc = walking_constraints
 
 let pf_get_new_id id gls = 
-  next_ident_away id (ids_of_sign (pf_untyped_hyps gls))
+  next_ident_away id (pf_ids_of_hyps gls)
 
 let pf_get_new_ids ids gls =
-  let avoid = ids_of_sign (pf_untyped_hyps gls) in
+  let avoid = pf_ids_of_hyps gls in
   List.fold_right
     (fun id acc -> (next_ident_away id (acc@avoid))::acc)
     ids []
@@ -93,7 +93,7 @@ let clenv_constrain_with_bindings bl clause =
 let add_prod_rel sigma (t,env) =
   match t with
     | DOP2(Prod,c1,(DLAM(na,b))) ->
-        (b,push_rel (na,Typing.execute_type env sigma c1) env)
+        (b,push_rel_decl (na,Retyping.get_assumption_of env sigma c1) env)
     | _ -> failwith "add_prod_rel"
 
 let rec add_prods_rel sigma (t,env) =