merging conflicts with the original "trunk__CLEANUP__Context__2" branch

3 files changed, 12 insertions, 8 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index ae2d059fa..2ed436c6b 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -15,6 +15,7 @@ open Tacmach
 open Util
 open Declarations
 open Globnames
+open Context.Rel.Declaration
 
 let qflag=ref true
 
@@ -139,8 +140,8 @@ let build_atoms gl metagen side cciterm =
 		  negative:= unsigned :: !negative
 	    end;
 	  let v = ind_hyps 0 i l gl in
-	  let g i _ (_,_,t) =
-	    build_rec env polarity (lift i t) in
+	  let g i _ decl =
+	    build_rec env polarity (lift i (get_type decl)) in
 	  let f l =
 	    List.fold_left_i g (1-(List.length l)) () l in
 	    if polarity && (* we have a constant constructor *)
@@ -150,8 +151,8 @@ let build_atoms gl metagen side cciterm =
       | Exists(i,l)->
 	  let var=mkMeta (metagen true) in
 	  let v =(ind_hyps 1 i l gl).(0) in
-	  let g i _ (_,_,t) =
-	    build_rec (var::env) polarity (lift i t) in
+	  let g i _ decl =
+	    build_rec (var::env) polarity (lift i (get_type decl)) in
 	    List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
@@ -224,7 +225,7 @@ let build_formula side nam typ gl metagen=
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
 		  | Exists (i,l) ->
-		      let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in
+		      let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in
 			Rexists(m,d,trivial)
 		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index fcbad46d4..0bc40136c 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -23,6 +23,7 @@ open Sequent
 open Names
 open Misctypes
 open Sigma.Notations
+open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
 	match inst1,inst2 with
@@ -120,7 +121,7 @@ let mk_open_instance id idc gl m t=
       let evmap = Sigma.Unsafe.of_evar_map evmap in
       let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
       let evmap = Sigma.to_evar_map evmap in
-      let decl = (Name nid,None,c) in
+      let decl = LocalAssum (Name nid, c) in
 	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m [] env evmap [] in
     evmap, decls, revt
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index d539eda57..c05015c53 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -19,6 +19,7 @@ open Formula
 open Sequent
 open Globnames
 open Locus
+open Context.Named.Declaration
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
@@ -34,12 +35,13 @@ let wrap n b continue seq gls=
     if i<=0 then seq else
       match nc with
 	  []->anomaly (Pp.str "Not the expected number of hyps")
-	| ((id,_,typ) as nd)::q->
+	| nd::q->
+            let id = get_id nd in
 	    if occur_var env id (pf_concl gls) ||
 	      List.exists (occur_var_in_decl env id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in
+	      add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in
   let seq1=aux n nc [] in
   let seq2=if b then
     add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in