- Reforme de la gestion des args recursifs (via arbres reguliers)

- coqtop -byte -opt bouclait!


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

1 files changed, 14 insertions, 1 deletions

diff --git a/kernel/sign.ml b/kernel/sign.ml
index 20bd1e03a6..e1c9fbe4b0 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -20,13 +20,19 @@ type named_context = named_declaration list
 
 let empty_named_context = []
 
-let add_named_decl d sign = d::sign
 
 let rec lookup_named id = function
   | (id',_,_ as decl) :: _ when id=id' -> decl
   | _ :: sign -> lookup_named id sign
   | [] -> raise Not_found
 
+  
+let add_named_decl (id,_,_ as d) sign =
+  try
+    let _ = lookup_named id sign in 
+    failwith ("identifier "^string_of_id id^" already defined")
+  with _ -> d::sign
+
 let named_context_length = List.length
 
 let pop_named_decl id = function
@@ -66,6 +72,13 @@ let lookup_rel n sign =
 
 let rel_context_length = List.length
 
+let rel_context_nhyps hyps =
+  let rec nhyps acc = function
+    | [] -> acc
+    | (_,None,_)::hyps -> nhyps (1+acc) hyps
+    | (_,Some _,_)::hyps -> nhyps acc hyps in
+  nhyps 0 hyps
+
 let fold_rel_context f l ~init:x = List.fold_right f l x
 let fold_rel_context_reverse f ~init:x l = List.fold_left f x l