gros commit de tout ce que j'ai fait pendant les vacances :

 - tactics/Equality
 - debug du discharge
 - constr_of_compattern implante vite fait / mal fait en attendant mieux
 - theories/Logic (ne passe pas entierrement)


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

2 files changed, 56 insertions, 7 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 989b786381..087cdb711b 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -513,9 +513,6 @@ let constr_of_com sigma env com =
 let constr_of_com_sort sigma sign com =
   constr_of_com1 true sigma sign com
 
-let constr_of_com_pattern sigma sign com =
-  constr_of_com1 true sigma sign com
-
 let fconstr_of_com1 is_ass sigma env com = 
   fconstr_of_com_env1 is_ass sigma env com
 
@@ -560,13 +557,61 @@ let fconstruct_with_univ sigma sign com =
   j
 *)
 
-open Closure
-open Tacred
+(* To process patterns, we need a translation from AST to term
+   without typing at all. *)
+
+let ctxt_of_ids ids =
+  Array.of_list (List.map (function id -> VAR id) ids)
+
+let constr_of_ref vars = function
+  | RConst (sp,ids) -> DOPN (Const sp, ctxt_of_ids ids)
+  | RInd (ip,ids) -> DOPN (MutInd ip, ctxt_of_ids ids)
+  | RConstruct (cp,ids) -> DOPN (MutConstruct cp, ctxt_of_ids ids)
+  | RAbst sp -> DOPN (Abst sp, [||])
+  | RVar id -> 
+      (try Rel (list_index (Name id) vars) with Not_found -> VAR id)
+  | REVar (n,ids) -> DOPN (Evar n, ctxt_of_ids ids)
+  | RMeta n -> DOP0 (Meta n)
+
+let constr_of_rawconstr c = 
+  let rec glob vars = function
+    | RRef (_,r) -> 
+	constr_of_ref vars r
+    | RApp (_,c,cl) -> 
+	let l = List.map (glob vars) (c::cl) in
+	DOPN (AppL, Array.of_list l)
+    | RBinder (_,BProd,na,c1,c2) ->
+	DOP2 (Prod, glob vars c1, DLAM (na, glob (na::vars) c2))
+    | RBinder (_,BLambda,na,c1,c2) ->
+	DOP2 (Lambda, glob vars c1, DLAM (na, glob (na::vars) c2))
+    | RSort (_,RProp c) ->
+	DOP0 (Sort (Prop c))
+    | RSort (_,RType) ->
+	DOP0 (Sort (Type (Univ.dummy_univ)))
+    | RHole _ -> 
+	DOP0 (Meta (new_meta()))
+    | RCast (_,c1,c2) ->
+	DOP2 (Cast, glob vars c1, glob vars c2)
+    | _ ->
+	error "constr_of_rawconstr: not implemented"
+  in
+  glob [] c
+
+let constr_of_com_pattern sigma env com = 
+  let c = raw_constr_of_com sigma (context env) com in
+  try 
+    constr_of_rawconstr c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
+
 
 (* Translation of reduction expression: we need trad because of Fold
  * Moreover, reduction expressions are used both in tactics and in
  * vernac. *)
 
+open Closure
+open Tacred
+
 let glob_nvar com =
   let s = nvar_of_ast com in
   try 
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 3e522f95cc..2fc7063373 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -289,8 +289,10 @@ let rec print_library_entry with_values ent =
   match ent with
     | (sp,Lib.Leaf lobj) -> 
 	[< print_leaf_entry with_values sep (sp,lobj) >]
-    | (_,Lib.OpenedSection (str,_)) -> 
+    | (_,Lib.OpenedSection str) -> 
         [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >]
+    | (_,Lib.ClosedSection (str,_)) -> 
+        [< 'sTR(" >>>>>>> Closed Section " ^ str); 'fNL >]
     | (_,Lib.Module str) ->
 	[< 'sTR(" >>>>>>> Module " ^ str); 'fNL >]
     | (_,Lib.FrozenState _) ->
@@ -386,6 +388,8 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name =
 
     | (_, (Lib.OpenedSection _ | Lib.FrozenState _ | Lib.Module _))::rest -> 
 	crible_rec rest
+    | (_, Lib.ClosedSection _) :: rest ->
+	crible_rec rest
     | []      -> ()
   in 
   try 
@@ -400,7 +404,7 @@ let print_crible name =
 
 let read_sec_context sec =
   let rec get_cxt in_cxt = function
-    | ((sp,Lib.OpenedSection (str,_)) as hd)::rest ->
+    | ((sp,Lib.OpenedSection str) as hd)::rest ->
         if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | [] -> []
     | hd::rest -> get_cxt (hd::in_cxt) rest