Abstraction de l'implémentation des signatures de Sign en vue intégration du let-in

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

4 files changed, 26 insertions, 31 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 353472f019..668d16b305 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -155,10 +155,9 @@ let new_meta_variables =
 let mk_assumption env sigma c = execute_type env sigma c
 				   
 let sign_before id = 
-  let rec aux = function
-    | [],[] -> error "no such hypothesis"
-    | sign -> 
-	if fst(hd_sign sign) = id then tl_sign sign else aux (tl_sign sign)
+  let rec aux sign =
+    if isnull_sign sign then error "no such hypothesis";
+    if fst (hd_sign sign) = id then tl_sign sign else aux (tl_sign sign)
   in 
   aux
 
@@ -373,18 +372,17 @@ let prim_refiner r sigma goal =
 	  error "convert-hyp rule passed non-converting term"
 	    
     | { name = Thin; hypspecs = ids } ->
-     	let rec remove_pair s = function
-          | ([],[]) -> 
-	      error ((string_of_id s) ^ " is not among the assumptions.")
-	  | sign -> 
-	      let (s',ty),tlsign = uncons_sign sign in
-	      if s = s' then 
-		tlsign
-              else if occur_var s ty.body then 
-		error ((string_of_id s) ^ " is used in the hypothesis " 
-		       ^ (string_of_id s'))
-              else 
-		add_sign (s',ty) (remove_pair s tlsign)
+     	let rec remove_pair s sign =
+	  if isnull_sign sign then
+	    error ((string_of_id s) ^ " is not among the assumptions.");
+	  let (s',ty),tlsign = uncons_sign sign in
+	  if s = s' then 
+	    tlsign
+          else if occur_var s ty.body then 
+	    error ((string_of_id s) ^ " is used in the hypothesis " 
+		   ^ (string_of_id s'))
+          else 
+	    add_sign (s',ty) (remove_pair s tlsign)
 	in
 	let clear_aux sign s =
           if occur_var s cl then
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index ffb88d104c..a02ee4faef 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -313,8 +313,8 @@ let pr_seq evd =
     | Some i -> i 
     | None -> anomaly "pr_seq : info = None"
   in
-  let (x,y) as hyps = var_context env in
-  let sign = List.rev(List.combine x y) in
+  let hyps = var_context env in
+  let sign = List.rev (list_of_sign hyps) in
   let pc = pr_ctxt info in
   let pdcl =
     prlist_with_sep pr_spc
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index c4cab5b6b9..3c8e390584 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -260,8 +260,7 @@ let extract_open_proof sign pf =
     | {ref=Some(Local_constraints lc,[pf])} -> (proof_extractor vl) pf
 	  
     | {ref=None;goal=goal} ->
-	let rel_env = get_rels vl in
-	let n_rels = List.length rel_env in
+	let n_rels = number_of_rels vl in
 	let visible_rels =
           map_succeed
             (fun id ->
@@ -811,14 +810,13 @@ let pr_rule = function
   | Context ctxt -> pr_ctxt ctxt
   | Local_constraints lc -> [< 'sTR"Local constraint change" >]
 
-let thin_sign osign (x,y) =
-  let com_nsign = List.combine x y in 
-  List.split
-    (map_succeed (fun (id,ty) ->
-                    if (not (mem_sign osign id))
-                      or (id,ty) <> (lookup_sign id osign) then
-                        (id,ty)
-                    else failwith "caught") com_nsign)
+let thin_sign osign sign =
+  sign_it
+    (fun id ty nsign ->
+       if (not (mem_sign osign id))
+         or (id,ty) <> (lookup_sign id osign)  (* Hum, egalité sur les types *)
+       then add_sign (id,ty) nsign
+       else nsign) sign nil_sign
 
 let rec print_proof sigma osign pf =
   let {evar_env=env; evar_concl=cl; 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 446d70b437..5a7c105947 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -45,9 +45,8 @@ let pf_hyps gls = var_context (sig_it gls).evar_env
 let pf_concl gls = (sig_it gls).evar_concl
 
 let pf_untyped_hyps gls  =
-  let env = pf_env gls in
-  let (idl,tyl) = Environ.var_context env in 
-  (idl, List.map (fun x -> x.body) tyl)
+  let sign = Environ.var_context (pf_env gls) in
+  map_sign_typ (fun x -> x.body) sign
 
 let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n