mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4

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

14 files changed, 235 insertions, 199 deletions

diff --git a/contrib/correctness/Permut.v b/contrib/correctness/ArrayPermut.v
index 0963c2b14..d183df49c 100644
--- a/contrib/correctness/Permut.v
+++ b/contrib/correctness/ArrayPermut.v
@@ -69,7 +69,7 @@ Hints Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym sub_permut_t
  *)
 
 Definition array_id := [n:Z][A:Set][t,t':(array n A)][g,d:Z]
-  (i:Z) `g <= i <= d` -> t#[i] = t'#[i].
+  (i:Z) `g <= i <= d` -> #t[i] = #t'[i].
 
 (* array_id is an equivalence relation *)
 
@@ -101,7 +101,7 @@ Lemma array_id_trans :
     -> (array_id t t'' g d).
 Proof.
 Unfold array_id. Intros.
-Apply trans_eq with y:=t'#[i]; Auto with datatypes.
+Apply trans_eq with y:=#t'[i]; Auto with datatypes.
 Save.
 
 Hints Resolve array_id_trans: v62 datatypes.
@@ -128,7 +128,7 @@ Hints Resolve sub_permut_id.
 Lemma sub_permut_eq :
   (n:Z)(A:Set)(t,t':(array n A))(g,d:Z)
   (sub_permut g d t t') ->
-  (i:Z) (`0<=i<g` \/ `d<i<n`) -> t#[i]=t'#[i].
+  (i:Z) (`0<=i<g` \/ `d<i<n`) -> #t[i]=#t'[i].
 Proof.
 Intros n A t t' g d Htt' i Hi.
 Elim (sub_permut_id Htt'). Unfold array_id. 
diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v
index 6fe72671a..794131428 100644
--- a/contrib/correctness/Arrays.v
+++ b/contrib/correctness/Arrays.v
@@ -64,19 +64,17 @@ Hints Resolve new_def store_def_1 store_def_2 : datatypes v62.
 
 (* A tactic to simplify access in arrays *)
 
-Tactic Definition ArrayAccess [$i $j $H] :=
- [<:tactic: <
-    Elim (Z_eq_dec $i $j); [ 
-      Intro $H; Rewrite $H; Rewrite store_def_1
-    | Intro $H; Rewrite store_def_2; [ Idtac | Idtac | Idtac | Exact $H ] ]
-  >>].
+Tactic Definition ArrayAccess i j H :=
+    Elim (Z_eq_dec i j); [ 
+      Intro H; Rewrite H; Rewrite store_def_1
+    | Intro H; Rewrite store_def_2; [ Idtac | Idtac | Idtac | Exact H ] ].
 
 (* Syntax and pretty-print for arrays *)
 
-Grammar command command0 :=
+Grammar constr constr0 :=
   array_access
-    [ ident($t) "#" "[" command($c) "]" ] -> [ <<(access $t $c)>> ].
+    [ "#" ident($t) "[" constr($c) "]" ] -> [ (access $t $c) ].
 
 Syntax constr level 0 :
   array_access
-    [ (APPLIST <<access>> ($VAR $t) $c) ] -> [ $t "#[" $c:L "]" ].
+    [ << (APPLIST access ($VAR $t) $c) >> ] -> [ $t "#[" $c:L "]" ].
diff --git a/contrib/correctness/Arrays_stuff.v b/contrib/correctness/Arrays_stuff.v
index edb3c8058..184602c57 100644
--- a/contrib/correctness/Arrays_stuff.v
+++ b/contrib/correctness/Arrays_stuff.v
@@ -11,6 +11,6 @@
 (* $Id$ *)
 
 Require Export Exchange.
-Require Export Permut.
+Require Export ArrayPermut.
 Require Export Sorted.
 
diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v
index 2a449ba25..ddad80b35 100644
--- a/contrib/correctness/Exchange.v
+++ b/contrib/correctness/Exchange.v
@@ -25,23 +25,23 @@ Implicit Arguments On.
 Inductive exchange [n:Z; A:Set; t,t':(array n A); i,j:Z] : Prop :=
   exchange_c :
     `0<=i<n` -> `0<=j<n` ->
-    (t#[i] = t'#[j]) ->
-    (t#[j] = t'#[i]) ->
-    ((k:Z)`0<=k<n` -> `k<>i` -> `k<>j` -> t#[k] = t'#[k]) ->
+    (#t[i] = #t'[j]) ->
+    (#t[j] = #t'[i]) ->
+    ((k:Z)`0<=k<n` -> `k<>i` -> `k<>j` -> #t[k] = #t'[k]) ->
     (exchange t t' i j).
     
 (* Properties about exchanges *)
 
 Lemma exchange_1 : (n:Z)(A:Set)(t:(array n A))
   (i,j:Z) `0<=i<n` -> `0<=j<n` ->
-  (access (store (store t i t#[j]) j t#[i]) i)=t#[j].
+  (access (store (store t i #t[j]) j #t[i]) i) = #t[j].
 Proof.
 Intros n A t i j H_i H_j.
 Case (dec_eq j i).
 Intro eq_i_j. Rewrite eq_i_j.
 Auto with datatypes.
 Intro not_j_i.
-Rewrite (store_def_2 (store t i t#[j]) t#[i] H_j H_i not_j_i).
+Rewrite (store_def_2 (store t i #t[j]) #t[i] H_j H_i not_j_i).
 Auto with datatypes.
 Save.
 
diff --git a/contrib/correctness/ProgramsExtraction.v b/contrib/correctness/ProgramsExtraction.v
index 23394dc18..8458105b4 100644
--- a/contrib/correctness/ProgramsExtraction.v
+++ b/contrib/correctness/ProgramsExtraction.v
@@ -16,11 +16,11 @@ Extract Inductive unit => unit [ "()" ].
 Extract Inductive bool => bool [ true false ].
 Extract Inductive sumbool => bool [ true false ].
 
-Require Export Programs.
+Require Export Correctness.
 
-Declare ML Module "prog_extract".
+Declare ML Module "pextract".
 
-Grammar vernac vernac :=
+Grammar vernac vernac : ast :=
   imperative_ocaml [ "Write" "Caml" "File" stringarg($file) 
     "[" ne_identarg_list($idl) "]" "." ]
      -> [ (IMPERATIVEEXTRACTION $file (VERNACARGLIST ($LIST $idl))) ]
diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v
index 9c99d6ed5..287d1dbeb 100644
--- a/contrib/correctness/Sorted.v
+++ b/contrib/correctness/Sorted.v
@@ -11,7 +11,7 @@
 (* $Id$ *)
 
 Require Export Arrays.
-Require Permut.
+Require ArrayPermut.
 
 Require ZArithRing.
 Require Omega.
@@ -22,7 +22,7 @@ Implicit Arguments On.
 
 Definition sorted_array :=
   [N:Z][A:(array N Z)][deb:Z][fin:Z]
-     `deb<=fin` -> (x:Z) `x>=deb` -> `x<fin` -> (Zle A#[x] A#[`x+1`]).
+     `deb<=fin` -> (x:Z) `x>=deb` -> `x<fin` -> (Zle #A[x] #A[`x+1`]).
 
 (* Elements of a sorted sub-array are in increasing order *)
 
@@ -87,7 +87,7 @@ Hints Resolve sub_sorted_array : datatypes v62.
 
 Lemma left_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z)
    `i>0` -> `j<N` -> (sorted_array A i j) 
-   -> (Zle A#[`i-1`]  A#[i]) -> (sorted_array A `i-1` j).
+   -> (Zle #A[`i-1`]  #A[i]) -> (sorted_array A `i-1` j).
 Proof.
 (Intros; Unfold sorted_array ; Intros).
 Elim (Z_ge_lt_dec x i).   (* (`x >= i`) + (`x < i`) *)
@@ -105,7 +105,7 @@ Save.
 
 Lemma right_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z)
    `i>=0` -> `j<N-1` -> (sorted_array A i j) 
-   -> (Zle A#[j]  A#[`j+1`]) -> (sorted_array A i `j+1`).
+   -> (Zle #A[j]  #A[`j+1`]) -> (sorted_array A i `j+1`).
 Proof.
 (Intros; Unfold sorted_array ; Intros).
 Elim (Z_lt_ge_dec x j).
@@ -121,7 +121,7 @@ Save.
 Lemma left_substitution : 
    (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z)
    `i>=0`  -> `j<N`  -> (sorted_array A i j)
-   -> (Zle v A#[i])
+   -> (Zle v #A[i])
    -> (sorted_array (store A i v) i j).
 Proof.
 Intros N A i j v H_i H_j H_sorted H_v.
@@ -145,7 +145,7 @@ Save.
 Lemma right_substitution : 
    (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z)
    `i>=0`  -> `j<N`  -> (sorted_array A i j)
-   -> (Zle A#[j] v)
+   -> (Zle #A[j] v)
    -> (sorted_array (store A j v) i j).
 Proof.
 Intros N A i j v H_i H_j H_sorted H_v.
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 0435095fa..950bc62bf 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -16,10 +16,11 @@ open Names
 open Term
 open Himsg
 
-open Putil
 open Ptype
 open Past
 
+let is_mutable = function Ref _ | Array _ -> true | _ -> false
+let is_pure = function TypePure _ -> true | _ -> false
 
 let raise_with_loc = function
   | None -> raise
diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml
index 03f9b30e1..a097ac1b5 100644
--- a/contrib/correctness/pextract.ml
+++ b/contrib/correctness/pextract.ml
@@ -17,29 +17,27 @@ open System
 open Names
 open Term
 open Himsg
-open Termenv
 open Reduction
 
-open Genpp
-
-open Mutil
-open Ptypes
+open Putil
+open Ptype
 open Past
 open Penv
 open Putil
 
 let extraction env c =
   let ren = initial_renaming env in
-  let sign = TradEnv.now_sign_of ren env in
+  let sign = Pcicenv.now_sign_of ren env in
   let fsign = Mach.fsign_of_sign (Evd.mt_evd()) sign in
-    match Mach.infexecute (Evd.mt_evd()) (sign,fsign) c with
-	(_,Inf j) -> j._VAL
-      | (_,Logic) -> failwith "Prog_extract.pp: should be informative"
+  match Mach.infexecute (Evd.mt_evd()) (sign,fsign) c with
+    | (_,Inf j) -> j._VAL
+    | (_,Logic) -> failwith "Prog_extract.pp: should be informative"
 
 (* les tableaux jouent un role particulier, puisqu'ils seront extraits
  * vers des tableaux ML *)
 
-let sp_access = path_of_string "#Arrays#access.fw"
+let sp_access = coq_constant ["correctness"; "Arrays"] "access"
+let access = ConstRef sp_access
 
 let has_array = ref false
 
@@ -63,8 +61,8 @@ let int_of_z = function
 let spset_of_cci env c =
   let spl = Fw_env.collect (extraction env c) in
   let sps = List.fold_left (fun e x -> SpSet.add x e) SpSet.empty spl in
-    has_array := !has_array or (SpSet.mem sp_access sps);
-    SpSet.remove sp_access sps
+  has_array := !has_array or (SpSet.mem sp_access sps);
+  SpSet.remove sp_access sps
 
 
 (* collect all Coq constants and all pgms appearing in a given program *)
@@ -79,7 +77,7 @@ let add_id env ((sp,ids) as s) id =
 
 let collect env =
   let rec collect_desc env s = function
-      Var x -> add_id env s x
+    | Var x -> add_id env s x
     | Acc x -> add_id env s x
     | Aff (x,e1) -> add_id env (collect_rec env s e1) x
     | TabAcc (_,x,e1) ->
@@ -133,7 +131,7 @@ let collect env =
   and collect_rec env s p = collect_desc env s p.desc
 
   in
-    collect_rec env (SpSet.empty,IdSet.empty)
+  collect_rec env (SpSet.empty,IdSet.empty)
 
 
 (* On a besoin de faire du renommage, tout comme pour l'extraction des
@@ -146,8 +144,8 @@ module Ocaml_ren = Ocaml.OCaml_renaming
 
 let rename_global id =
   let id' = Ocaml_ren.rename_global_term !Fwtoml.globals (Name id) in
-    Fwtoml.add_global_renaming (id,id');
-    id'
+  Fwtoml.add_global_renaming (id,id');
+  id'
 
 type rename_struct = { rn_map : identifier IdMap.t;
 		       rn_avoid : identifier list }
@@ -156,8 +154,8 @@ let rn_empty = { rn_map = IdMap.empty; rn_avoid = [] }
 
 let rename_local rn id =
   let id' = Ocaml_ren.rename_term (!Fwtoml.globals@rn.rn_avoid) (Name id) in
-    { rn_map = IdMap.add id id' rn.rn_map; rn_avoid = id' :: rn.rn_avoid },
-    id'
+  { rn_map = IdMap.add id id' rn.rn_map; rn_avoid = id' :: rn.rn_avoid },
+  id'
 
 let get_local_name rn id = IdMap.find id rn.rn_map
 
@@ -168,8 +166,8 @@ let get_name env rn id =
     Fwtoml.get_global_name id
 
 let rec rename_binders rn = function
-    [] -> rn
-  | (id,_)::bl -> let rn',_ = rename_local rn id in rename_binders rn' bl
+  | [] -> rn
+  | (id,_) :: bl -> let rn',_ = rename_local rn id in rename_binders rn' bl
 
 (* on a bespoin d'un pretty-printer de constr particulier, qui reconnaisse
  * les acces a des references et dans des tableaux, et qui de plus n'imprime
@@ -188,7 +186,7 @@ let is_ref env id =
     Not_found -> false
 
 let rec pp_constr env rn = function
-    VAR id ->
+  | VAR id ->
       if is_ref env id then 
 	[< 'sTR"!"; pID (get_name env rn id) >] 
       else
@@ -214,21 +212,22 @@ let rec pp_constr env rn = function
 (* pretty-print of imperative programs *)
 
 let collect_lambda = 
- let rec collect acc p = match p.desc with
-     Lam(bl,t) -> collect (bl@acc) t
-   | x         -> acc,p
- in collect []
+  let rec collect acc p = match p.desc with
+    | Lam(bl,t) -> collect (bl@acc) t
+    | x         -> acc,p
+  in 
+  collect []
 
 let pr_binding rn = 
   prlist_with_sep (fun () -> [< >])
     (function 
-	 (id,(Untyped | BindType _)) -> 
+       | (id,(Untyped | BindType _)) -> 
 	   [< 'sTR" "; pID (get_local_name rn id) >]
        | (id,BindSet) -> [< >])
 
 let pp_prog id =
   let rec pp_d env rn par = function
-      Var x -> pID (get_name env rn x)
+    | Var x -> pID (get_name env rn x)
     | Acc x -> [< 'sTR"!"; pID (get_name env rn x) >]
     | Aff (x,e1) -> [< pID (get_name env rn x); 
 		       'sTR" := "; hOV 0 (pp env rn false e1) >]
@@ -325,7 +324,7 @@ let pp_prog id =
     [< pp_d env rn par p.desc >]
 
   and pp_mut v c = match v with
-      Ref _ ->
+    | Ref _ ->
 	[< 'sTR"ref "; pp_constr empty rn_empty (extraction empty c) >]
     | Array (n,_) ->
 	[< 'sTR"Array.create "; 'cUT;
@@ -341,13 +340,13 @@ let pp_prog id =
       try
 	let c = find_init id in
 	hOV 0 [< 'sTR"let "; pID id'; 'sTR" = "; pp_mut v c >]
-      with
-	  Not_found -> errorlabstrm "Prog_extract.pp_prog"
-	      [< 'sTR"The variable "; pID id;
-		 'sTR" must be initialized first !" >]
+      with Not_found -> 
+	errorlabstrm "Prog_extract.pp_prog"
+	  [< 'sTR"The variable "; pID id;
+	     'sTR" must be initialized first !" >]
     else
       match find_pgm id with
-	  None -> 
+	| None -> 
 	    errorlabstrm "Prog_extract.pp_prog"
 	      [< 'sTR"The program "; pID id;
 		 'sTR" must be realized first !" >]
@@ -355,8 +354,8 @@ let pp_prog id =
 	    let bl,p = collect_lambda p in
 	    let rn = rename_binders rn_empty bl in
 	    let env = traverse_binders empty bl in
-	      hOV 0  [< 'sTR"let "; pID id'; pr_binding rn bl; 'sTR" ="; 'fNL; 
-			'sTR"  "; hOV 2 (pp env rn false p) >]
+	    hOV 0  [< 'sTR"let "; pID id'; pr_binding rn bl; 'sTR" ="; 'fNL; 
+		      'sTR"  "; hOV 2 (pp env rn false p) >]
 
 (* extraction des programmes impératifs/fonctionnels vers ocaml *)
 
@@ -367,14 +366,13 @@ let pp_prog id =
  * de ml_import.fwsp_of_id
  *)
 
-let import sp =
-  match repr_path sp with
-      [m],_,_ ->
-	begin
-	  try Library.import_export_module m true
-          with _ -> ()
-	end
-    | _ -> ()
+let import sp = match repr_path sp with
+  | [m],_,_ ->
+      begin
+	try Library.import_export_module m true
+        with _ -> ()
+      end
+  | _ -> ()
 
 let pp_ocaml file prm =
   has_array := false;
@@ -388,31 +386,31 @@ let pp_ocaml file prm =
   (* on met les programmes dans l'ordre et pour chacun on recherche les
    * objects Coq necessaires, que l'on rajoute a l'ensemble cic *)
   let cic,_,pgms =
-    let o_pgms = fold_all (fun (id,_) l -> id::l) empty []
-    in
-      List.fold_left
-      	(fun (cic,pgms,pl) id -> 
-	   if IdSet.mem id pgms then
-	     let spl,pgms' =
-	       try
-		 (match find_pgm id with
-		      Some p -> collect empty p
-		    | None ->
-			(try 
-			   let c = find_init id in
-			     spset_of_cci empty c,IdSet.empty
-			 with Not_found -> SpSet.empty,IdSet.empty))
-	       with Not_found -> SpSet.empty,IdSet.empty
-	     in
-	     let cic' = 
-	       SpSet.fold 
-		 (fun sp cic -> import sp; IdSet.add (basename sp) cic)
-		 spl cic
-	     in
-	     (cic',IdSet.union pgms pgms',id::pl)
-	   else
-	     (cic,pgms,pl)) 
-      	 (cic,pgms,[]) o_pgms
+    let o_pgms = fold_all (fun (id,_) l -> id::l) empty [] in
+    List.fold_left
+      (fun (cic,pgms,pl) id -> 
+	 if IdSet.mem id pgms then
+	   let spl,pgms' =
+	     try
+	       (match find_pgm id with
+		  | Some p -> collect empty p
+		  | None ->
+		      (try 
+			 let c = find_init id in
+			 spset_of_cci empty c,IdSet.empty
+		       with Not_found -> 
+			 SpSet.empty,IdSet.empty))
+	     with Not_found -> SpSet.empty,IdSet.empty
+	   in
+	   let cic' = 
+	     SpSet.fold 
+	       (fun sp cic -> import sp; IdSet.add (basename sp) cic)
+	       spl cic
+	   in
+	   (cic',IdSet.union pgms pgms',id::pl)
+	 else
+	   (cic,pgms,pl)) 
+      (cic,pgms,[]) o_pgms
   in
   let cic = IdSet.elements cic in
   (* on pretty-print *)
@@ -429,10 +427,12 @@ let pp_ocaml file prm =
   (* puis on ecrit dans le fichier *)
   let chan = open_trapping_failure open_out file ".ml" in
   let ft = with_output_to chan in
-    (try  pP_with ft strm ; pp_flush_with ft ()
-     with e -> pp_flush_with ft () ; close_out chan; raise e);
-    close_out chan
-
+  begin
+    try  pP_with ft strm ; pp_flush_with ft ()
+    with e -> pp_flush_with ft () ; close_out chan; raise e
+  end;
+  close_out chan
+    
 
 (* Initializations of mutable objects *)
 
@@ -440,32 +440,33 @@ let initialize id com =
   let loc = Ast.loc com in
   let c = constr_of_com (Evd.mt_evd()) (initial_sign()) com in
   let ty = type_of (Evd.mt_evd()) (initial_sign()) c in
-    try
-      let v = lookup_global id in
-      let ety = match v with Ref (TypePure c) -> c | Array (_,TypePure c) -> c
-	                    | _ -> raise Not_found in
-	if conv (Evd.mt_evd()) ty ety then
-	  initialize id c
-	else
-	  errorlabstrm "Prog_extract.initialize"
-	    [< 'sTR"Not the expected type for the mutable "; pID id >]
-    with
-	Not_found -> errorlabstrm "Prog_extract.initialize"
-	    [< pID id; 'sTR" is not a mutable" >]
+  try
+    let v = lookup_global id in
+    let ety = match v with 
+      | Ref (TypePure c) -> c | Array (_,TypePure c) -> c
+      | _ -> raise Not_found 
+    in
+    if conv (Evd.mt_evd()) ty ety then
+      initialize id c
+    else
+      errorlabstrm "Prog_extract.initialize"
+	[< 'sTR"Not the expected type for the mutable "; pID id >]
+  with Not_found -> 
+    errorlabstrm "Prog_extract.initialize"
+      [< pr_id id; 'sTR" is not a mutable" >]
 
 (* grammaire *)
 
-open Vernacinterp;;
-
-overwriting_vinterp_add("IMPERATIVEEXTRACTION",
-	    function VARG_STRING file :: rem ->
-	      let prm = parse_param rem in
-	      	(fun () -> pp_ocaml file prm)
-    | _ -> anomaly "IMPERATIVEEXTRACTION called with bad arguments.")
-;;
-
-overwriting_vinterp_add("INITIALIZE",
-	    function [VARG_IDENTIFIER id ; VARG_COMMAND com] ->
-	      fun () -> initialize id com
-    | _ -> anomaly "INITIALIZE called with bad arguments.")
-;;
+open Vernacinterp
+
+let _ = vinterp_add "IMPERATIVEEXTRACTION"
+	  (function 
+	     | VARG_STRING file :: rem ->
+		 let prm = parse_param rem in (fun () -> pp_ocaml file prm)
+	     | _ -> assert false)
+	  
+let _ = vinterp_add "INITIALIZE"
+	  (function 
+	     | [VARG_IDENTIFIER id ; VARG_COMMAND com] ->
+		 (fun () -> initialize id com)
+	     | _ -> assert false)
diff --git a/contrib/correctness/pextract.mli b/contrib/correctness/pextract.mli
index 433fc33f2..76b779213 100644
--- a/contrib/correctness/pextract.mli
+++ b/contrib/correctness/pextract.mli
@@ -11,8 +11,7 @@
 (* $Id$ *)
 
 open Names
-open Genpp
 
-val pp_ocaml : string -> extraction_params -> unit
+val pp_ocaml : string -> unit
 
 
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index 6dbf1e460..9d69ecdcb 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -178,6 +178,11 @@ let make_abs bl t = match bl with
  * if there is no yi and no post-condition, it is simplified in res itself.
  *)
 
+let simple_constr_of_prog = function
+  | CC_expr c -> c
+  | CC_var id -> mkVar id
+  | _ -> assert false
+
 let make_tuple l q ren env before = match l with
   | [e,_] when q = None -> 
       e
@@ -186,7 +191,7 @@ let make_tuple l q ren env before = match l with
       let dep,h,th = match q with
 	| None -> false,[],[]
 	| Some c ->
-	    let args = List.map (fun (e,_) -> constr_of_prog e) l in
+	    let args = List.map (fun (e,_) -> simple_constr_of_prog e) l in
 	    let c = apply_post ren env before c in
 	    true,
 	    [ CC_hole (Term.applist (c.a_value, args)) ], (* hole *)
@@ -219,7 +224,7 @@ let result_tuple ren before env (res,v) (ef,q) =
 
 let let_in_pre ty p t =
   let h = p.p_value in
-  CC_letin (false, ty, [pre_name p.p_name,CC_typed_binder h], (CC_hole h,h), t)
+  CC_letin (false, ty, [pre_name p.p_name,CC_typed_binder h], CC_hole h, t)
 
 let multiple_let_in_pre ty hl t =
   List.fold_left (fun t h -> let_in_pre ty h t) t hl
@@ -236,7 +241,7 @@ let make_let_in ren env fe p (vo,q) (res,tyres) (t,ty) =
     let name = match q with None -> product_name n | _ -> dep_product_name n in
     constant name 
   in
-  let t = CC_letin (dep, ty, bl, (fe,tyapp), t) in
+  let t = CC_letin (dep, ty, bl, fe, t) in
   multiple_let_in_pre ty (List.map (apply_pre ren env) p) t
 
 
@@ -404,7 +409,7 @@ let make_if_case ren env ty (b,qb) (br1,br2) =
     	Term.mkLambda (name, t1, (mkArrow t2 ty)), q.a_name
     | None -> assert false
   in
-  CC_app (CC_case (ty', (b, constant "bool"), [br1;br2]),
+  CC_app (CC_case (ty', b, [br1;br2]),
 	  [CC_var (post_name id_b)])
 
 let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c =
diff --git a/contrib/correctness/preuves.v b/contrib/correctness/preuves.v
index 757669c67..22eccbdba 100644
--- a/contrib/correctness/preuves.v
+++ b/contrib/correctness/preuves.v
@@ -3,29 +3,43 @@
  * juste histoire d'avoir un petit bench.
  *)
 
-Require Programs.
+Require Correctness.
 Require Omega.
 
-Prog Variable x : Z ref.
-Prog Variable y : Z ref.
-Prog Variable z : Z ref.
-Prog Variable i : Z ref.
-Prog Variable j : Z ref.
-Prog Variable n : Z ref.
-Prog Variable m : Z ref.
+Global Variable x : Z ref.
+Global Variable y : Z ref.
+Global Variable z : Z ref.
+Global Variable i : Z ref.
+Global Variable j : Z ref.
+Global Variable n : Z ref.
+Global Variable m : Z ref.
 Variable r : Z.
 Variable N : Z.
-Prog Variable t : array N of Z.
+Global Variable t : array N of Z.
 
+(**********************************************************************)
+
+Global Variable x : Z ref.
+Debug on.
+Correctness assign0 (x := 0) { `x=0` }.
+Save.
+
+(**********************************************************************)
+
+Global Variable i : Z ref.
+Debug on.
+Correctness assign1 { `0 <= i` } begin i := !i + 1 end { `0 < i` }.
+
+(**********************************************************************)
 
 (**********************************************************************)
 
 Correctness echange
   { `0 <= i < N` /\ `0 <= j < N` }
   begin
-    state B;
+    label B;
     x := t[!i]; t[!i] := t[!j]; t[!j] := !x;
-    assert { t#[i] = t@B#[j] /\ t#[j] = t@B#[i] }
+    assert { #t[i] = #t@B[j] /\ #t[j] = #t@B[i] }
   end.
 Proof.
 Auto.
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index aa6daffe6..64a291026 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -230,18 +230,18 @@ GEXTEND Gram
   ;
   type_v2:
     [ LEFTA
-      [ v = type_v2; LIDENT "ref" -> Ref v
+      [ v = type_v2; IDENT "ref" -> Ref v
       | t = type_v3 -> t ] ]
   ;
   type_v3:
-    [ [ LIDENT "array"; size = Constr.constr; "of"; v = type_v0 ->
+    [ [ IDENT "array"; size = Constr.constr; "of"; v = type_v0 ->
           Array (size,v)
-      | LIDENT "fun"; bl = binders; c = type_c -> make_arrow bl c
+      | IDENT "fun"; bl = binders; c = type_c -> make_arrow bl c
       | c = Constr.constr -> TypePure c	  
       ] ]
   ;
   type_c:
-    [ [ LIDENT "returns"; id = LIDENT; ":"; v = type_v;
+    [ [ IDENT "returns"; id = IDENT; ":"; v = type_v;
         e = effects; p = OPT pre_condition; q = OPT post_condition; "end" ->
         ((id_of_string id, v), e, list_of_some p, q)
       ] ] 
@@ -256,21 +256,21 @@ GEXTEND Gram
       ] ]
   ;
   reads:
-    [ [ LIDENT "reads"; l = LIST0 LIDENT SEP "," -> List.map id_of_string l ] ]
+    [ [ IDENT "reads"; l = LIST0 IDENT SEP "," -> List.map id_of_string l ] ]
   ;
   writes:
-    [ [ LIDENT "writes"; l=LIST0 LIDENT SEP "," -> List.map id_of_string l ] ]
+    [ [ IDENT "writes"; l=LIST0 IDENT SEP "," -> List.map id_of_string l ] ]
   ;
   pre_condition:
-    [ [ LIDENT "pre"; c = predicate -> pre_of_assert false c ] ]
+    [ [ IDENT "pre"; c = predicate -> pre_of_assert false c ] ]
   ;
   post_condition:
-    [ [ LIDENT "post"; c = predicate -> c ] ]
+    [ [ IDENT "post"; c = predicate -> c ] ]
   ;
 
   (* Binders (for both types and programs) **********************************)
   binder:
-    [ [ "("; sl = LIST1 LIDENT SEP ","; ":"; t = binder_type ; ")" ->
+    [ [ "("; sl = LIST1 IDENT SEP ","; ":"; t = binder_type ; ")" ->
 	  List.map (fun s -> (id_of_string s, t)) sl
       ] ]
   ;
@@ -288,17 +288,17 @@ GEXTEND Gram
     [ [ c = Constr.constr; n = name -> { a_name = n; a_value = c } ] ]
   ;
   name:
-    [ [ "as"; s = LIDENT -> Name (id_of_string s)
+    [ [ "as"; s = IDENT -> Name (id_of_string s)
       | -> Anonymous
       ] ]
   ;
 
   (* Programs ***************************************************************)
   variable:
-    [ [ s = LIDENT -> id_of_string s ] ]
+    [ [ s = IDENT -> id_of_string s ] ]
   ;
   ident:
-    [ [ s = LIDENT -> id_of_string s ] ]
+    [ [ s = IDENT -> id_of_string s ] ]
   ;
   assertion:
     [ [ "{"; c = predicate; "}" -> c ] ]
@@ -338,13 +338,13 @@ GEXTEND Gram
   ;
 
   ast1:
-    [ [ x = prog2; LIDENT "or"; y = prog1  -> bool_or loc x y
-      | x = prog2; LIDENT "and"; y = prog1 -> bool_and loc x y
+    [ [ x = prog2; IDENT "or"; y = prog1  -> bool_or loc x y
+      | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y
       | x = prog2 -> x
       ] ]
   ;
   ast2:
-    [ [ LIDENT "not"; x = prog3 -> bool_not loc x
+    [ [ IDENT "not"; x = prog3 -> bool_not loc x
       | x = prog3 -> x
       ] ]
   ;
@@ -386,35 +386,35 @@ GEXTEND Gram
 	  TabAff (true,v,e,p)
       | v = variable; "#"; "["; e = program; "]"; ":="; p = program -> 
 	  TabAff (true,v,e,p)
-      | LIDENT "if"; e1 = program; LIDENT "then"; e2 = program;
-	LIDENT "else"; e3 = program ->
+      | IDENT "if"; e1 = program; IDENT "then"; e2 = program;
+	IDENT "else"; e3 = program ->
 	  If (e1,e2,e3)
-      | LIDENT "if"; e1 = program; LIDENT "then"; e2 = program ->
+      | IDENT "if"; e1 = program; IDENT "then"; e2 = program ->
 	  If (e1,e2,without_effect loc (Expression (constant "tt")))
-      | LIDENT "while"; b = program; LIDENT "do"; 
-	"{"; inv = OPT invariant; LIDENT "variant"; wf = variant; "}";
-	bl = block; LIDENT "done" ->
+      | IDENT "while"; b = program; IDENT "do"; 
+	"{"; inv = OPT invariant; IDENT "variant"; wf = variant; "}";
+	bl = block; IDENT "done" ->
 	  While (b, inv, wf, bl)
-      | LIDENT "for"; i = LIDENT; "="; v1 = program; LIDENT "to"; v2 = program;
-	LIDENT "do"; "{"; inv = invariant; "}"; 
-	bl = block; LIDENT "done" -> 
+      | IDENT "for"; i = IDENT; "="; v1 = program; IDENT "to"; v2 = program;
+	IDENT "do"; "{"; inv = invariant; "}"; 
+	bl = block; IDENT "done" -> 
 	  make_ast_for loc i v1 v2 inv bl
-      | LIDENT "let"; v = variable; "="; LIDENT "ref"; p1 = program;
+      | IDENT "let"; v = variable; "="; IDENT "ref"; p1 = program;
 	"in"; p2 = program ->
 	  LetRef (v, p1, p2)
-      | LIDENT "let"; v = variable; "="; p1 = program; "in"; p2 = program ->
+      | IDENT "let"; v = variable; "="; p1 = program; "in"; p2 = program ->
 	  LetIn (v, p1, p2)
-      | LIDENT "begin"; b = block; "end" ->
+      | IDENT "begin"; b = block; "end" ->
 	  Seq b
-      | LIDENT "fun"; bl = binders; "->"; p = program ->
+      | IDENT "fun"; bl = binders; "->"; p = program ->
 	  Lam (bl,p)
-      | LIDENT "let"; LIDENT "rec"; f = variable; 
+      | IDENT "let"; IDENT "rec"; f = variable; 
 	bl = binders; ":"; v = type_v;
-	"{"; LIDENT "variant"; var = variant; "}"; "="; p = program ->
+	"{"; IDENT "variant"; var = variant; "}"; "="; p = program ->
 	  LetRec (f,bl,v,var,p)
-      | LIDENT "let"; LIDENT "rec"; f = variable; 
+      | IDENT "let"; IDENT "rec"; f = variable; 
 	bl = binders; ":"; v = type_v;
-	"{"; LIDENT "variant"; var = variant; "}"; "="; p = program;
+	"{"; IDENT "variant"; var = variant; "}"; "="; p = program;
  	"in"; p2 = program ->
 	  LetIn (f, without_effect loc (LetRec (f,bl,v,var,p)), p2)
 
@@ -441,8 +441,8 @@ GEXTEND Gram
       | s = block_statement                 -> [s] ] ]
   ;
   block_statement:
-    [ [ LIDENT "label"; s = LIDENT -> Label s
-      | LIDENT "assert"; c = assertion -> Assert c 
+    [ [ IDENT "label"; s = IDENT -> Label s
+      | IDENT "assert"; c = assertion -> Assert c 
       | p = program -> Statement p ] ]
   ;
   relation:
@@ -456,17 +456,17 @@ GEXTEND Gram
 
   (* Other entries (invariants, etc.) ***************************************)
   wf_arg:
-    [ [ "{"; LIDENT "wf"; c = Constr.constr; LIDENT "for";
+    [ [ "{"; IDENT "wf"; c = Constr.constr; IDENT "for";
 	w = Constr.constr; "}" ->
 	  Wf (c,w)
-      | "{"; LIDENT "wf"; n = INT; "}" ->
+      | "{"; IDENT "wf"; n = INT; "}" ->
 	  RecArg (int_of_string n) ] ]
   ;
   invariant:
-    [ [ LIDENT "invariant"; c = predicate -> c ] ]
+    [ [ IDENT "invariant"; c = predicate -> c ] ]
   ;
   variant:
-    [ [ c = Constr.constr; LIDENT "for"; r = Constr.constr -> (c, r)
+    [ [ c = Constr.constr; IDENT "for"; r = Constr.constr -> (c, r)
       | c = Constr.constr -> (c, ast_zwf_zero loc) ] ]
   ;
   END
@@ -550,30 +550,30 @@ let _ = add "PROGVARIABLE"
 open Vernac
 
 GEXTEND Gram
-  Pcoq.Vernac.vernac:
-  [ [ LIDENT "Global"; "Variable"; 
-      l = LIST1 LIDENT SEP ","; ":"; t = type_v; "." ->
+  Pcoq.Vernac_.vernac:
+  [ [ IDENT "Global"; "Variable"; 
+      l = LIST1 IDENT SEP ","; ":"; t = type_v; "." ->
 	let idl = List.map Ast.nvar l in
 	let d = Ast.dynamic (in_typev t) in
 	  <:ast< (PROGVARIABLE (VERNACARGLIST ($LIST $idl)) (VERNACDYN $d)) >>
 
-    | LIDENT "Show"; LIDENT "Programs"; "." ->
+    | IDENT "Show"; IDENT "Programs"; "." ->
 	<:ast< (SHOWPROGRAMS) >>
 
-    | LIDENT "Correctness"; s = LIDENT; p = Programs.program; "." ->
+    | IDENT "Correctness"; s = IDENT; p = Programs.program; "." ->
 	let d = Ast.dynamic (in_prog p) in
 	let str = Ast.str s in
 	<:ast< (CORRECTNESS $str (VERNACDYN $d)) >>
 
-     | LIDENT "Correctness"; s = LIDENT; p = Programs.program; ";";
-       tac = Tactic.tactic; "." ->
+    | IDENT "Correctness"; s = IDENT; p = Programs.program; ";";
+      tac = Tactic.tactic; "." ->
 	let d = Ast.dynamic (in_prog p) in
 	let str = Ast.str s in
 	<:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >>
 
-   | LIDENT "Debug"; LIDENT "on"; "." -> <:ast< (PROGDEBUGON) >>
-	    
-    | LIDENT "Debug"; LIDENT "off"; "." -> <:ast< (PROGDEBUGOFF) >>
+    | IDENT "Debug"; IDENT "on"; "." -> <:ast< (PROGDEBUGON) >>
+	
+    | IDENT "Debug"; IDENT "off"; "." -> <:ast< (PROGDEBUGOFF) >>
 	    
   ] ]
   ;
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index d92d8524b..b8ac08531 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -36,7 +36,7 @@ let coqast_of_prog p =
   let p = Pdb.db_prog p in
 
   (* 2. typage avec effets *)
-  deb_mess [< 'sTR"Ptyping.states: Typage avec effets..."; 'fNL >];
+  deb_mess [< 'sTR"Ptyping.states: Typing with effects..."; 'fNL >];
   let env = Penv.empty in
   let ren = initial_renaming env in
   let p = Ptyping.states ren env p in
@@ -53,20 +53,20 @@ let coqast_of_prog p =
 
   (* 4b. traduction terme (terme intermédiaire de type cc_term) *)
   deb_mess 
-    [< 'fNL; 'sTR"Mlise.trad: Traduction program -> cc_term..."; 'fNL >];
+    [< 'fNL; 'sTR"Mlize.trad: Translation program -> cc_term..."; 'fNL >];
   let cc = Pmlize.trans ren p in
   let cc = Pred.red cc in
   deb_mess (Putil.pp_cc_term cc);
 
   (* 5. traduction en constr *)
   deb_mess 
-    [< 'fNL; 'sTR"Pcic.constr_of_prog: Traduction cc_term -> constr..."; 
+    [< 'fNL; 'sTR"Pcic.constr_of_prog: Translation cc_term -> rawconstr..."; 
        'fNL >];
   let r = Pcic.rawconstr_of_prog cc in
   deb_mess (Printer.pr_rawterm r);
 
   (* 6. résolution implicites *)
-  deb_mess [< 'fNL; 'sTR"Résolution implicites (? => Meta(n))..."; 'fNL >];
+  deb_mess [< 'fNL; 'sTR"Resolution implicits (? => Meta(n))..."; 'fNL >];
   let oc = understand_gen_tcc Evd.empty (Global.env()) [] [] None r in
   deb_mess (Printer.prterm (snd oc));
 
@@ -195,6 +195,24 @@ let (automatic : tactic) =
  * Vernac: Correctness <string> <program> [; <tactic>].
  *)
 
+let reduce_open_constr (em,c) =
+  let existential_map_of_constr = 
+    let rec collect em c = match kind_of_term c with
+      | IsCast (c',t) -> 
+	  (match kind_of_term c' with
+	     | IsEvar ev -> (ev,t) :: em
+	     | _ -> fold_constr collect em c)
+      | IsEvar _ -> 
+	  assert false (* all existentials should be casted *)
+      | _ -> 
+	  fold_constr collect em c
+    in
+    collect []
+  in
+  let c = Pred.red_cci c in
+  let em = existential_map_of_constr c in
+  (em,c)
+
 let correctness s p opttac =
   Pmisc.reset_names();
   let p,oc,cty,v = coqast_of_prog p in
@@ -206,9 +224,9 @@ let correctness s p opttac =
   start_proof id Declare.NeverDischarge sign cty;
   Penv.new_edited id (v,p);
   if !debug then show_open_subgoals();
-  deb_mess [< 'sTR"Pred.red_cci: Réduction..."; 'fNL >];
-  let oc = let (mm,c) = oc in (mm, Pred.red_cci c) in
-  deb_mess [< 'sTR"APRES REDUCTION :"; 'fNL >];
+  deb_mess [< 'sTR"Pred.red_cci: Reduction..."; 'fNL >];
+  let oc = reduce_open_constr oc in
+  deb_mess [< 'sTR"AFTER REDUCTION:"; 'fNL >];
   deb_mess (Printer.prterm (snd oc));
   let tac = (tclTHEN (Refine.refine_tac oc) automatic) in
   let tac = match opttac with 
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index a5e7c81af..472cee1af 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Declare ML Module "mlutil.cmo" "ocaml.cmo" "extraction.cmo" "extract_env.cmo".
+Declare ML Module "mlutil" "ocaml" "extraction" "extract_env".
 
 Grammar vernac vernac : ast :=
   extr_constr [ "Extraction" constrarg($c) "." ] ->