From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 27 Apr 2005 17:01:49 +0000 (+0000)
Subject: merged changes from the svn fork by me and Enrico
X-Git-Tag: after_svn_merge~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0575a1cb077087970f311b48f2e45dc4a01a6867;p=helm.git

merged changes from the svn fork by me and Enrico
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 6f179505d..650b69723 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -106,6 +106,9 @@ let rec token' = lexer
 
 and token = lexer
 *)
+
+let remove_quotes s = String.sub s 1 (String.length s - 2)
+
 let rec token comments = lexer
   | blanks -> token comments lexbuf
   | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
@@ -119,9 +122,7 @@ let rec token comments = lexer
   | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
   | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf)
   | qstring ->
-      let lexeme = Ulexing.utf8_lexeme lexbuf in
-      let s = String.sub lexeme 1 (String.length lexeme - 2) in
-      return lexbuf ("QSTRING", s)
+      return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
   | symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
   | tex_token ->
       let macro =
diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index d32302a13..d7096ae79 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -65,12 +65,12 @@ let tactic = Grammar.Entry.create grammar "tactic"
 let tactical = Grammar.Entry.create grammar "tactical"
 let tactical0 = Grammar.Entry.create grammar "tactical0"
 let command = Grammar.Entry.create grammar "command"
+let alias_spec = Grammar.Entry.create grammar "alias_spec"
+let macro = Grammar.Entry.create grammar "macro"
 let script = Grammar.Entry.create grammar "script"
+let statement = Grammar.Entry.create grammar "statement"
 
 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
-let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic)
-let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
-let return_command loc cmd = cmd  (* TODO ZACK FIXME uhm ... why we drop loc? *)
 
 let fail floc msg =
   let (x, y) = CicAst.loc_of_floc floc in
@@ -88,6 +88,12 @@ let int_opt = function
   | None -> None
   | Some lexeme -> Some (int_of_string lexeme)
 
+let int_of_string s =
+  try
+    Pervasives.int_of_string s
+  with Failure _ ->
+    failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
+
   (** the uri of an inductive type (a ".ind" uri) is not meaningful without an
   * xpointer. Still, it's likely that an user who wrote "cic:/blabla/foo.ind"
   * actually meant "cic:/blabla/foo.ind#xpointer(1/1)", i.e. the first inductive
@@ -110,7 +116,7 @@ let mk_binder_ast binder typ vars body =
     vars body
 
 EXTEND
-  GLOBAL: term term0 tactic tactical tactical0 command script;
+  GLOBAL: term term0 statement;
   int: [
     [ num = NUM ->
         try
@@ -318,132 +324,126 @@ EXTEND
     [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
   ];
   reduction_kind: [
-    [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce
-    | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl
-    | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ]
+    [ [ IDENT "reduce" ] -> `Reduce
+    | [ IDENT "simplify" ] -> `Simpl
+    | [ IDENT "whd" ] -> `Whd ]
   ];
   tactic: [
-    [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
-        return_tactic loc (TacticAst.Absurd t)
-    | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term ->
-        return_tactic loc (TacticAst.Apply t)
-    | [ IDENT "assumption" | IDENT "Assumption" ] ->
-        return_tactic loc TacticAst.Assumption
-    | [ IDENT "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto
-    | [ IDENT "change" | IDENT "Change" ];
+    [ [ IDENT "absurd" ]; t = tactic_term ->
+        TacticAst.Absurd (loc, t)
+    | [ IDENT "apply" ]; t = tactic_term ->
+        TacticAst.Apply (loc, t)
+    | [ IDENT "assumption" ] ->
+        TacticAst.Assumption loc
+    | [ IDENT "auto" ] -> TacticAst.Auto loc
+    | [ IDENT "change" ];
       t1 = tactic_term; "with"; t2 = tactic_term;
       where = tactic_where ->
-        return_tactic loc (TacticAst.Change (t1, t2, where))
+        TacticAst.Change (loc, t1, t2, where)
     (* TODO Change_pattern *)
-    | [ IDENT "contradiction" | IDENT "Contradiction" ] ->
-        return_tactic loc TacticAst.Contradiction
-    | [ IDENT "cut" | IDENT "Cut" ];
-      t = tactic_term -> return_tactic loc (TacticAst.Cut t)
-    | [ IDENT "decompose" | IDENT "Decompose" ];
+    | [ IDENT "contradiction" ] ->
+        TacticAst.Contradiction loc
+    | [ IDENT "cut" ];
+      t = tactic_term ->
+        TacticAst.Cut (loc, t)
+    | [ IDENT "decompose" ];
       principles = ident_list1; where = IDENT ->
-        return_tactic loc (TacticAst.Decompose (where, principles))
-    | [ IDENT "discriminate" | IDENT "Discriminate" ];
+        TacticAst.Decompose (loc, where, principles)
+    | [ IDENT "discriminate" ];
       hyp = IDENT ->
-        return_tactic loc (TacticAst.Discriminate hyp)
-    | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term ->
-        return_tactic loc (TacticAst.ElimType t)
-    | [ IDENT "elim" | IDENT "Elim" ];
+        TacticAst.Discriminate (loc, hyp)
+    | [ IDENT "elimType" ]; t = tactic_term ->
+        TacticAst.ElimType (loc, t)
+    | [ IDENT "elim" ];
       t1 = tactic_term;
       using = OPT [ "using"; using = tactic_term -> using ] ->
-        return_tactic loc (TacticAst.Elim (t1, using))
-    | [ IDENT "exact" | IDENT "Exact" ]; t = tactic_term ->
-        return_tactic loc (TacticAst.Exact t)
-    | [ IDENT "exists" | IDENT "Exists" ] ->
-        return_tactic loc TacticAst.Exists
-    | [ IDENT "fold" | IDENT "Fold" ];
+        TacticAst.Elim (loc, t1, using)
+    | [ IDENT "exact" ]; t = tactic_term ->
+        TacticAst.Exact (loc, t)
+    | [ IDENT "exists" ] ->
+        TacticAst.Exists loc
+    | [ IDENT "fold" ];
       kind = reduction_kind; t = tactic_term ->
-        return_tactic loc (TacticAst.Fold (kind, t))
-    | [ IDENT "fourier" | IDENT "Fourier" ] ->
-        return_tactic loc TacticAst.Fourier
-    | [ IDENT "hint" | IDENT "Hint" ] -> return_tactic loc TacticAst.Hint
-    | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT ->
-        return_tactic loc (TacticAst.Injection ident)
-    | [ IDENT "intros" | IDENT "Intros" ];
+        TacticAst.Fold (loc, kind, t)
+    | [ IDENT "fourier" ] ->
+        TacticAst.Fourier loc
+    | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n)
+    | [ IDENT "hint" ] -> TacticAst.Hint loc
+    | [ IDENT "injection" ]; ident = IDENT ->
+        TacticAst.Injection (loc, ident)
+    | [ IDENT "intros" ];
       num = OPT [ num = int -> num ];
       idents = OPT ident_list0 ->
         let idents = match idents with None -> [] | Some idents -> idents in
-        return_tactic loc (TacticAst.Intros (num, idents))
-    | [ IDENT "intro" | IDENT "Intro" ] ->
-        return_tactic loc (TacticAst.Intros (None, []))
-    | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
+        TacticAst.Intros (loc, num, idents)
+    | [ IDENT "intro" ] ->
+        TacticAst.Intros (loc, None, [])
+    | [ IDENT "left" ] -> TacticAst.Left loc
     | [ "let" | "Let" ];
       t = tactic_term; "in"; where = IDENT ->
-        return_tactic loc (TacticAst.LetIn (t, where))
+        TacticAst.LetIn (loc, t, where)
     | kind = reduction_kind;
       pat = OPT [
         "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
           pat
       ];
       terms = LIST0 term SEP SYMBOL "," ->
-        let tac =
-          (match (pat, terms) with
-          | None, [] -> TacticAst.Reduce (kind, None)
-          | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
-          | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
-          | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
-        in
-        return_tactic loc tac
-    | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
-        return_tactic loc TacticAst.Reflexivity
-    | [ IDENT "replace" | IDENT "Replace" ];
+        (match (pat, terms) with
+        | None, [] -> TacticAst.Reduce (loc, kind, None)
+        | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
+        | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat))
+        | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
+    | [ IDENT "reflexivity" ] ->
+        TacticAst.Reflexivity loc
+    | [ IDENT "replace" ];
       t1 = tactic_term; "with"; t2 = tactic_term ->
-        return_tactic loc (TacticAst.Replace (t1, t2))
+        TacticAst.Replace (loc, t1, t2)
     (* TODO Rewrite *)
     (* TODO Replace_pattern *)
-    | [ IDENT "right" | IDENT "Right" ] -> return_tactic loc TacticAst.Right
-    | [ IDENT "ring" | IDENT "Ring" ] -> return_tactic loc TacticAst.Ring
-    | [ IDENT "split" | IDENT "Split" ] -> return_tactic loc TacticAst.Split
-    | [ IDENT "symmetry" | IDENT "Symmetry" ] ->
-        return_tactic loc TacticAst.Symmetry
-    | [ IDENT "transitivity" | IDENT "Transitivity" ];
+    | [ IDENT "right" ] -> TacticAst.Right loc
+    | [ IDENT "ring" ] -> TacticAst.Ring loc
+    | [ IDENT "split" ] -> TacticAst.Split loc
+    | [ IDENT "symmetry" ] ->
+        TacticAst.Symmetry loc
+    | [ IDENT "transitivity" ];
       t = tactic_term ->
-        return_tactic loc (TacticAst.Transitivity t)
+        TacticAst.Transitivity (loc, t)
     ]
   ];
-  tactical0: [ [ t = tactical; SYMBOL "." -> return_tactical loc t ] ];
   tactical:
-    [ "command" NONA
-      [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
-    | "sequence" LEFTA
-      [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
-          (match tactics with
-          | [tactic] -> tactic
-          | _ -> return_tactical loc (TacticAst.Seq tactics))
+    [ "sequence" LEFTA
+      [ tacticals = LIST1 NEXT SEP SYMBOL ";" ->
+          TacticAst.Seq (loc, tacticals)
       ]
     | "then" NONA
       [ tac = tactical;
         PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
-          return_tactical loc (TacticAst.Then (tac, tacs))
+          (TacticAst.Then (loc, tac, tacs))
       ]
     | "loops" RIGHTA
-      [ [ IDENT "do" | IDENT "Do" ]; count = int; tac = tactical ->
-          return_tactical loc (TacticAst.Do (count, tac))
-      | [ IDENT "repeat" | IDENT "Repeat" ]; tac = tactical ->
-          return_tactical loc (TacticAst.Repeat tac)
+      [ [ IDENT "do" ]; count = int; tac = tactical ->
+          TacticAst.Do (loc, count, tac)
+      | [ IDENT "repeat" ]; tac = tactical ->
+          TacticAst.Repeat (loc, tac)
       ]
     | "simple" NONA
-      [ [ IDENT "tries" | IDENT "Tries" ];
+      [ IDENT "tries";
         PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
-          return_tactical loc (TacticAst.Tries tacs)
-      | [ IDENT "try" | IDENT "Try" ]; tac = NEXT ->
-          return_tactical loc (TacticAst.Try tac)
-      | [ IDENT "fail" | IDENT "Fail" ] -> return_tactical loc TacticAst.Fail
-      | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac
-      | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
-      | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
+          TacticAst.Tries (loc, tacs)
+      | IDENT "try"; tac = NEXT ->
+          TacticAst.Try (loc, tac)
+      | IDENT "fail" -> TacticAst.Fail loc
+      | IDENT "id" -> TacticAst.IdTac loc
+      | PAREN "("; tac = tactical; PAREN ")" -> tac
+      | tac = tactic -> TacticAst.Tactic (loc, tac)
       ]
     ];
-  theorem_flavour: [  (* all flavours but Goal *)
-    [ [ IDENT "definition"  | IDENT "Definition"  ] -> `Definition
-    | [ IDENT "fact"        | IDENT "Fact"        ] -> `Fact
-    | [ IDENT "lemma"       | IDENT "Lemma"       ] -> `Lemma
-    | [ IDENT "remark"      | IDENT "Remark"      ] -> `Remark
-    | [ IDENT "theorem"     | IDENT "Theorem"     ] -> `Theorem
+  theorem_flavour: [
+    [ [ IDENT "definition"  ] -> `Definition
+    | [ IDENT "fact"        ] -> `Fact
+    | [ IDENT "lemma"       ] -> `Lemma
+    | [ IDENT "remark"      ] -> `Remark
+    | [ IDENT "theorem"     ] -> `Theorem
     ]
   ];
   inductive_spec: [ [
@@ -469,27 +469,63 @@ EXTEND
       let ind_types = fst_ind_type :: tl_ind_types in
       (params, ind_types)
   ] ];
-  print_kind: [
-    [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ]
-      -> `Env
-    | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ]
-      -> `Coer
-  ] ];
 
-  command: [
-    [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
-    | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
-    | [ IDENT "quit"  | IDENT "Quit"  ] -> return_command loc TacticAst.Quit
-    | [ IDENT "qed"   | IDENT "Qed"   ] ->
-        return_command loc (TacticAst.Qed None)
-    | [ IDENT "print"   | IDENT "Print" ];
-      print_kind = print_kind ->
-            return_command loc (TacticAst.Print print_kind)
-    | [ IDENT "save"  | IDENT "Save"  ]; name = IDENT ->
-        return_command loc (TacticAst.Qed (Some name))
+  macro: [[
+      [ IDENT "abort" ] -> TacticAst.Abort loc
+    | [ IDENT "quit"  ] -> TacticAst.Quit loc
+    | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
+    | [ IDENT "undo"   ]; steps = OPT NUM ->
+        TacticAst.Undo (loc, int_opt steps)
+    | [ IDENT "redo"   ]; steps = OPT NUM ->
+        TacticAst.Redo (loc, int_opt steps)
+    | [ IDENT "check"   ]; t = term ->
+        TacticAst.Check (loc, t)
+    | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
+  ]];
+
+  alias_spec: [
+    [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
+      let alpha = "[a-zA-Z]" in
+      let num = "[0-9]+" in
+      let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
+      let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
+      let rex = Str.regexp ("^"^ident^"$") in
+      if Str.string_match rex id 0 then
+        let rex = Str.regexp 
+          ("^\\(cic:/\\|theory:/\\)"^ident^
+           "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^
+           "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$") 
+        in
+        if Str.string_match rex uri 0 then
+          TacticAst.Ident_alias (id, uri)
+        else 
+          raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri))
+      else
+        raise (Parse_error (loc,sprintf "Not a valid identifier: %s" id))
+    | IDENT "symbol"; symbol = QSTRING;
+      instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ];
+      SYMBOL "="; dsc = QSTRING ->
+        let instance =
+          match instance with Some i -> int_of_string i | None -> 0
+        in
+        TacticAst.Symbol_alias (symbol, instance, dsc)
+    | IDENT "num";
+      instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ];
+      SYMBOL "="; dsc = QSTRING ->
+        let instance =
+          match instance with Some i -> int_of_string i | None -> 0
+        in
+        TacticAst.Number_alias (instance, dsc)
+    ]
+  ];
+  
+  command: [[
+      [ IDENT "set"    ]; n = QSTRING; v = QSTRING ->
+        TacticAst.Set (loc, n, v)
+    | [ IDENT "qed"   ] -> TacticAst.Qed loc
     | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
-        return_command loc (TacticAst.Theorem (flavour, name, typ, body))
+        TacticAst.Theorem (loc, flavour, name, typ, body)
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = let_defs -> 
           let name,ty = 
@@ -500,48 +536,33 @@ EXTEND
             | _ -> assert false 
           in
           let body = CicAst.Ident (name,None) in
-          TacticAst.Theorem(`Definition, Some name, ty,
+          TacticAst.Theorem(loc, `Definition, Some name, ty,
             Some (CicAst.LetRec (ind_kind, defs, body)))
           
-    | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec ->
+    | [ IDENT "inductive" ]; spec = inductive_spec ->
         let (params, ind_types) = spec in
-        return_command loc (TacticAst.Inductive (params, ind_types))
-    | [ IDENT "coinductive" | IDENT "CoInductive" ]; spec = inductive_spec ->
+        TacticAst.Inductive (loc, params, ind_types)
+    | [ IDENT "coinductive" ]; spec = inductive_spec ->
         let (params, ind_types) = spec in
         let ind_types = (* set inductive flags to false (coinductive) *)
           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
             ind_types
         in
-        return_command loc (TacticAst.Inductive (params, ind_types))
-    | [ IDENT "coercion" | IDENT "Coercion" ] ; name = IDENT -> 
-        return_command loc (TacticAst.Coercion (CicAst.Ident (name,Some [])))
-    | [ IDENT "coercion" | IDENT "Coercion" ] ; name = URI -> 
-        return_command loc (TacticAst.Coercion (CicAst.Uri (name,Some [])))
-    | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
-      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
-        return_command loc (TacticAst.Theorem (`Goal, None, typ, body))
-    | [ IDENT "undo"   | IDENT "Undo" ]; steps = OPT NUM ->
-        return_command loc (TacticAst.Undo (int_opt steps))
-    | [ IDENT "redo"   | IDENT "Redo" ]; steps = OPT NUM ->
-        return_command loc (TacticAst.Redo (int_opt steps))
-    | [ IDENT "baseuri"   | IDENT "Baseuri" ]; uri = OPT QSTRING ->
-        return_command loc (TacticAst.Baseuri uri)
-    | [ IDENT "basedir"   | IDENT "Basedir" ]; uri = OPT QSTRING ->
-        return_command loc (TacticAst.Basedir uri)
-    | [ IDENT "check"   | IDENT "Check" ]; t = term ->
-        return_command loc (TacticAst.Check t)
-(*
-    | [ IDENT "alias"   | IDENT "Alias" ]; spec = alias_spec ->
-        return_command loc (TacticAst.Alias spec)
-*)
-    ]
-  ];
-  script_entry: [
-    [ cmd = tactical0 -> Command cmd
-(*     | s = COMMENT -> Comment (loc, s) *)
+        TacticAst.Inductive (loc, params, ind_types)
+    | [ IDENT "coercion" ] ; name = IDENT -> 
+        TacticAst.Coercion (loc, CicAst.Ident (name,Some []))
+    | [ IDENT "coercion" ] ; name = URI -> 
+        TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
+    | [ IDENT "alias"   ]; spec = alias_spec ->
+        TacticAst.Alias (loc, spec)
+  ]];
+
+  statement: [
+    [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd)
+    | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac)
+    | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac)
     ]
   ];
-  script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ];
 END
 
 let exc_located_wrapper f =
@@ -555,12 +576,8 @@ let exc_located_wrapper f =
 
 let parse_term stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
-let parse_tactic stream =
-  exc_located_wrapper (fun () -> (Grammar.Entry.parse tactic stream))
-let parse_tactical stream =
-  exc_located_wrapper (fun () -> (Grammar.Entry.parse tactical0 stream))
-let parse_script stream =
-  exc_located_wrapper (fun () -> (Grammar.Entry.parse script stream))
+let parse_statement stream =
+  exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
 
 (**/**)
 
@@ -581,12 +598,13 @@ module EnvironmentP3 =
           (fun domain_item (dsc, _) acc ->
             let s =
               match domain_item with
-              | Id id -> sprintf "alias id %s = %s" id dsc
-              | Symbol (symb, instance) ->
-                  sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
-                    symb instance dsc
-              | Num instance ->
-                  sprintf "alias num (instance %d) = \"%s\"" instance dsc
+              | Id id ->
+                  TacticAstPp.pp_alias (TacticAst.Ident_alias (id, dsc)) ^ "."
+              | Symbol (symb, i) ->
+                  TacticAstPp.pp_alias (TacticAst.Symbol_alias (symb, i, dsc))
+                  ^ "."
+              | Num i ->
+                  TacticAstPp.pp_alias (TacticAst.Number_alias (i, dsc)) ^ "."
             in
             s :: acc)
           env []
diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
index 659bb2aa5..f7510a9bd 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
@@ -27,10 +27,8 @@ exception Parse_error of Token.flocation * string
 
 (** {2 Parsing functions} *)
 
-val parse_term:     char Stream.t -> DisambiguateTypes.term
-val parse_tactic:   char Stream.t -> DisambiguateTypes.tactic
-val parse_tactical: char Stream.t -> DisambiguateTypes.tactical
-val parse_script:   char Stream.t -> DisambiguateTypes.script
+val parse_term:       char Stream.t -> DisambiguateTypes.term
+val parse_statement:  char Stream.t -> (CicAst.term, string) TacticAst.statement
 
 (** {2 Grammar extensions} *)
 
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 54478c81a..552e3d30b 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -417,6 +417,21 @@ let domain_diff dom1 dom2 =
   in
   List.filter (fun elt -> not (is_in_dom2 elt)) dom1
 
+module type Disambiguator =
+sig
+  val disambiguate_term :
+    dbd:Mysql.dbd ->
+    context:Cic.context ->
+    metasenv:Cic.metasenv ->
+    ?initial_ugraph:CicUniv.universe_graph -> 
+    aliases:environment ->  (* previous interpretation status *)
+    CicAst.term ->
+    (environment *                   (* new interpretation status *)
+     Cic.metasenv *                  (* new metasenv *)
+     Cic.term*
+     CicUniv.universe_graph) list    (* disambiguated term *)
+end
+
 module Make (C: Callbacks) =
   struct
     let choices_of_id dbd id =
@@ -449,8 +464,9 @@ module Make (C: Callbacks) =
            fun _ _ _ -> term))
         uris
 
-    let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
+    let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv
       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+      term
     =
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
@@ -625,8 +641,8 @@ struct
         ?(aliases=DisambiguateTypes.Environment.empty) term =
     let ast = CicTextualParser2.parse_term (Stream.of_string term) in
     try
-      Disambiguator.disambiguate_term ~dbd context metasenv ast ?initial_ugraph
-        ~aliases
+      Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+        ?initial_ugraph ~aliases
     with Exit -> raise (Ambiguous_term term)
 end
 
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 3eff90ad6..ac9b97792 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -29,20 +29,22 @@ open DisambiguateTypes
 
 exception NoWellTypedInterpretation
 
-module Make (C : Callbacks) :
-  sig
-    val disambiguate_term :
-      dbd:Mysql.dbd ->
-      Cic.context ->
-      Cic.metasenv ->
-      CicAst.term ->
-      ?initial_ugraph:CicUniv.universe_graph -> 
-      aliases:environment ->  (* previous interpretation status *)
-      (environment *                   (* new interpretation status *)
-       Cic.metasenv *                  (* new metasenv *)
-       Cic.term*
-       CicUniv.universe_graph) list    (* disambiguated term *)
-  end
+module type Disambiguator =
+sig
+  val disambiguate_term :
+    dbd:Mysql.dbd ->
+    context:Cic.context ->
+    metasenv:Cic.metasenv ->
+    ?initial_ugraph:CicUniv.universe_graph -> 
+    aliases:environment ->  (* previous interpretation status *)
+    CicAst.term ->
+    (environment *                   (* new interpretation status *)
+     Cic.metasenv *                  (* new metasenv *)
+     Cic.term*
+     CicUniv.universe_graph) list    (* disambiguated term *)
+end
+
+module Make (C : Callbacks) : Disambiguator
 
 module Trivial:
 sig
diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml
index 356c0a369..31bcdad05 100644
--- a/helm/ocaml/cic_disambiguation/test_parser.ml
+++ b/helm/ocaml/cic_disambiguation/test_parser.ml
@@ -30,17 +30,16 @@ let pp_tactical = TacticAst2Box.tacticalPp
 let mode =
   try
     match Sys.argv.(1) with
-    | "alias" -> prerr_endline "Alias"; `Alias
     | "term" -> prerr_endline "Term"; `Term
-    | "tactic" -> prerr_endline "Tactic"; `Tactic
-    | "tactical" | "command" -> prerr_endline "Tactical"; `Tactical
-    | "script" -> prerr_endline "Script"; `Script
+    | "statement" -> prerr_endline "Statement"; `Statement
+(*     | "script" -> prerr_endline "Script"; `Script *)
     | _ ->
         prerr_endline "What???????";
         exit 1
   with Invalid_argument _ -> prerr_endline "Term"; `Term
 
 let _ =
+(*
   if mode = `Script then
     let ic = open_in Sys.argv.(2) in
     let istream = Stream.of_channel ic in
@@ -51,6 +50,7 @@ let _ =
         | DisambiguateTypes.Comment (loc, s) -> print_endline s)
       script
   else
+*)
     let ic = stdin in
     try
       while true do
@@ -61,12 +61,17 @@ let _ =
           | `Term ->
               let term = CicTextualParser2.parse_term istream in
               print_endline (BoxPp.pp_term term)
-          | `Tactic ->
-              let tac = CicTextualParser2.parse_tactic istream in
-              print_endline (TacticAstPp.pp_tactic tac)
+          | `Statement ->
+              (match CicTextualParser2.parse_statement istream with
+              | TacticAst.Command (_, cmd) ->
+                  print_endline (TacticAstPp.pp_command cmd)
+              | TacticAst.Tactical (_, tac) ->
+                  print_endline (TacticAstPp.pp_tactical tac))
+(*
           | `Tactical ->
               let tac = CicTextualParser2.parse_tactical istream in
               print_endline (pp_tactical tac)
+*)
           | `Alias ->
               let env = CicTextualParser2.EnvironmentP3.of_string line in
               print_endline (CicTextualParser2.EnvironmentP3.to_string env)
diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 128da869b..6bfced57e 100644
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -367,9 +367,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
            function
               [] -> []
             | (Some (n,C.Decl t))::tl ->
-               (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
             | (Some (n,C.Def (t,None)))::tl ->
-               (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::
+               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
                 (aux (i+1) tl)
             | None::tl -> None::(aux (i+1) tl)
             | (Some (_,C.Def (_,Some _)))::_ -> assert false
@@ -398,7 +398,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           in
            let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
             (* Checks suppressed *)
-            CicSubstitution.lift_meta l ty
+            CicSubstitution.subst_meta l ty
      | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
          C.Sort (C.Type (CicUniv.fresh()))
      | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend
index c212f6cad..09359d63a 100644
--- a/helm/ocaml/cic_proof_checking/.depend
+++ b/helm/ocaml/cic_proof_checking/.depend
@@ -1,19 +1,15 @@
 cicLogger.cmo: cicLogger.cmi 
 cicLogger.cmx: cicLogger.cmi 
-cicEnvironment.cmo: cicLogger.cmi cicEnvironment.cmi 
-cicEnvironment.cmx: cicLogger.cmx cicEnvironment.cmi 
-cicUnivUtils.cmo: cicEnvironment.cmi cicUnivUtils.cmi 
-cicUnivUtils.cmx: cicEnvironment.cmx cicUnivUtils.cmi 
+cicEnvironment.cmo: cicEnvironment.cmi 
+cicEnvironment.cmx: cicEnvironment.cmi 
 cicPp.cmo: cicEnvironment.cmi cicPp.cmi 
 cicPp.cmx: cicEnvironment.cmx cicPp.cmi 
+cicUnivUtils.cmo: cicEnvironment.cmi cicUnivUtils.cmi 
+cicUnivUtils.cmx: cicEnvironment.cmx cicUnivUtils.cmi 
 cicSubstitution.cmo: cicEnvironment.cmi cicSubstitution.cmi 
 cicSubstitution.cmx: cicEnvironment.cmx cicSubstitution.cmi 
 cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi 
 cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi 
-cicReductionNaif.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \
-    cicReductionNaif.cmi 
-cicReductionNaif.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \
-    cicReductionNaif.cmi 
 cicReduction.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \
     cicReduction.cmi 
 cicReduction.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \
@@ -22,5 +18,7 @@ cicTypeChecker.cmo: cicSubstitution.cmi cicReduction.cmi cicPp.cmi \
     cicLogger.cmi cicEnvironment.cmi cicTypeChecker.cmi 
 cicTypeChecker.cmx: cicSubstitution.cmx cicReduction.cmx cicPp.cmx \
     cicLogger.cmx cicEnvironment.cmx cicTypeChecker.cmi 
-cicElim.cmo: cicSubstitution.cmi cicEnvironment.cmi cicElim.cmi 
-cicElim.cmx: cicSubstitution.cmx cicEnvironment.cmx cicElim.cmi 
+cicElim.cmo: cicTypeChecker.cmi cicSubstitution.cmi cicReduction.cmi \
+    cicPp.cmi cicEnvironment.cmi cicElim.cmi 
+cicElim.cmx: cicTypeChecker.cmx cicSubstitution.cmx cicReduction.cmx \
+    cicPp.cmx cicEnvironment.cmx cicElim.cmi 
diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile
index 95657131f..de106143c 100644
--- a/helm/ocaml/cic_proof_checking/Makefile
+++ b/helm/ocaml/cic_proof_checking/Makefile
@@ -12,7 +12,6 @@ INTERFACE_FILES = \
 	cicUnivUtils.mli \
 	cicSubstitution.mli \
 	cicMiniReduction.mli \
-	cicReductionNaif.mli \
 	cicReduction.mli \
 	cicTypeChecker.mli \
 	cicElim.mli
@@ -34,14 +33,6 @@ all_utilities:
 opt_utilities:
 	$(MAKE) -C utilities/ opt
 
-cicReduction.ml: $(REDUCTION_IMPLEMENTATION)
-	if ! [ -f $@ ]; then \
-		echo "Using $< for $@";	\
-		ln -s $< $@;	\
-	else	\
-		true;	\
-	fi
-
 clean: clean_utilities
 clean_utilities:
 	$(MAKE) -C utilities/ clean
diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index fe87fc4af..ce6a7f225 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -83,7 +83,7 @@ val add_type_checked_term :
   UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
 
   (** remove a type checked object
-  * @raise Term_not_found when given term is not in the environment
+  * @raise Object_not_found when given term is not in the environment
   * @raise Failure when remove_term is invoked while type checking *)
 val remove_obj: UriManager.uri -> unit
 
diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
new file mode 100644
index 000000000..687a46549
--- /dev/null
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -0,0 +1,1036 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* TODO unify exceptions *)
+
+exception CicReductionInternalError;;
+exception WrongUriToInductiveDefinition;;
+exception Impossible of int;;
+exception ReferenceToConstant;;
+exception ReferenceToVariable;;
+exception ReferenceToCurrentProof;;
+exception ReferenceToInductiveDefinition;;
+
+let fdebug = ref 1;;
+let debug t env s =
+ let rec debug_aux t i =
+  let module C = Cic in
+  let module U = UriManager in
+   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
+ in
+  if !fdebug = 0 then
+   prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
+;;
+
+module type Strategy =
+ sig
+  type stack_term
+  type env_term
+  type ens_term
+  val to_stack : Cic.term -> stack_term
+  val to_stack_list : Cic.term list -> stack_term list
+  val to_env : Cic.term -> env_term
+  val to_ens : Cic.term -> ens_term
+  val from_stack :
+   unwind:
+    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+      Cic.term -> Cic.term) ->
+   stack_term -> Cic.term
+  val from_stack_list :
+   unwind:
+    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+      Cic.term -> Cic.term) ->
+   stack_term list -> Cic.term list
+  val from_env : env_term -> Cic.term
+  val from_ens : ens_term -> Cic.term
+  val stack_to_env :
+   reduce:
+    (int * env_term list * ens_term Cic.explicit_named_substitution *
+      Cic.term * stack_term list -> Cic.term) ->
+   unwind:
+    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+      Cic.term -> Cic.term) ->
+   stack_term -> env_term
+  val compute_to_env :
+   reduce:
+    (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
+      stack_term list -> Cic.term) ->
+   unwind:
+    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+      Cic.term -> Cic.term) ->
+   int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+    Cic.term -> env_term
+  val compute_to_stack :
+   reduce:
+    (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
+      stack_term list -> Cic.term) ->
+   unwind:
+    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+      Cic.term -> Cic.term) ->
+   int -> env_term list -> ens_term Cic.explicit_named_substitution ->
+    Cic.term -> stack_term
+ end
+;;
+
+module CallByNameStrategy =
+ struct
+  type stack_term = Cic.term
+  type env_term = Cic.term
+  type ens_term = Cic.term
+  let to_stack v = v
+  let to_stack_list l = l
+  let to_env v = v
+  let to_ens v = v
+  let from_stack ~unwind v = v
+  let from_stack_list ~unwind l = l
+  let from_env v = v
+  let from_ens v = v
+  let stack_to_env ~reduce ~unwind v = v
+  let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
+  let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
+ end
+;;
+
+module CallByValueStrategy =
+ struct
+  type stack_term = Cic.term
+  type env_term = Cic.term
+  type ens_term = Cic.term
+  let to_stack v = v
+  let to_stack_list l = l
+  let to_env v = v
+  let to_ens v = v
+  let from_stack ~unwind v = v
+  let from_stack_list ~unwind l = l
+  let from_env v = v
+  let from_ens v = v
+  let stack_to_env ~reduce ~unwind v = v
+  let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
+  let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
+ end
+;;
+
+module CallByValueStrategyByNameOnConstants =
+ struct
+  type stack_term = Cic.term
+  type env_term = Cic.term
+  type ens_term = Cic.term
+  let to_stack v = v
+  let to_stack_list l = l
+  let to_env v = v
+  let to_ens v = v
+  let from_stack ~unwind v = v
+  let from_stack_list ~unwind l = l
+  let from_env v = v
+  let from_ens v = v
+  let stack_to_env ~reduce ~unwind v = v
+  let compute_to_stack ~reduce ~unwind k e ens =
+   function
+      Cic.Const _ as t -> unwind k e ens t    
+    | t -> reduce (k,e,ens,t,[])
+  let compute_to_env ~reduce ~unwind k e ens =
+   function
+      Cic.Const _ as t -> unwind k e ens t    
+    | t -> reduce (k,e,ens,t,[])
+ end
+;;
+
+module LazyCallByValueStrategy =
+ struct
+  type stack_term = Cic.term lazy_t
+  type env_term = Cic.term lazy_t
+  type ens_term = Cic.term lazy_t
+  let to_stack v = lazy v
+  let to_stack_list l = List.map to_stack l
+  let to_env v = lazy v
+  let to_ens v = lazy v
+  let from_stack ~unwind v = Lazy.force v
+  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+  let from_env v = Lazy.force v
+  let from_ens v = Lazy.force v
+  let stack_to_env ~reduce ~unwind v = v
+  let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
+  let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
+ end
+;;
+
+module LazyCallByValueStrategyByNameOnConstants =
+ struct
+  type stack_term = Cic.term lazy_t
+  type env_term = Cic.term lazy_t
+  type ens_term = Cic.term lazy_t
+  let to_stack v = lazy v
+  let to_stack_list l = List.map to_stack l
+  let to_env v = lazy v
+  let to_ens v = lazy v
+  let from_stack ~unwind v = Lazy.force v
+  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+  let from_env v = Lazy.force v
+  let from_ens v = Lazy.force v
+  let stack_to_env ~reduce ~unwind v = v
+  let compute_to_stack ~reduce ~unwind k e ens t =
+   lazy (
+    match t with
+       Cic.Const _ as t -> unwind k e ens t    
+     | t -> reduce (k,e,ens,t,[]))
+  let compute_to_env ~reduce ~unwind k e ens t =
+   lazy (
+    match t with
+       Cic.Const _ as t -> unwind k e ens t    
+     | t -> reduce (k,e,ens,t,[]))
+ end
+;;
+
+module LazyCallByNameStrategy =
+ struct
+  type stack_term = Cic.term lazy_t
+  type env_term = Cic.term lazy_t
+  type ens_term = Cic.term lazy_t
+  let to_stack v = lazy v
+  let to_stack_list l = List.map to_stack l
+  let to_env v = lazy v
+  let to_ens v = lazy v
+  let from_stack ~unwind v = Lazy.force v
+  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+  let from_env v = Lazy.force v
+  let from_ens v = Lazy.force v
+  let stack_to_env ~reduce ~unwind v = v
+  let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
+  let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
+ end
+;;
+
+module
+ LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
+=
+ struct
+  type stack_term = reduce:bool -> Cic.term
+  type env_term = reduce:bool -> Cic.term
+  type ens_term = reduce:bool -> Cic.term
+  let to_stack v =
+   let value = lazy v in
+    fun ~reduce -> Lazy.force value
+  let to_stack_list l = List.map to_stack l
+  let to_env v =
+   let value = lazy v in
+    fun ~reduce -> Lazy.force value
+  let to_ens v =
+   let value = lazy v in
+    fun ~reduce -> Lazy.force value
+  let from_stack ~unwind v = (v ~reduce:false)
+  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+  let from_env v = (v ~reduce:true)
+  let from_ens v = (v ~reduce:true)
+  let stack_to_env ~reduce ~unwind v = v
+  let compute_to_stack ~reduce ~unwind k e ens t =
+   let svalue =
+     lazy (
+      match t with
+         Cic.Const _ as t -> unwind k e ens t    
+       | t -> reduce (k,e,ens,t,[])
+     ) in
+   let lvalue =
+    lazy (unwind k e ens t)
+   in
+    fun ~reduce ->
+     if reduce then Lazy.force svalue else Lazy.force lvalue
+  let compute_to_env ~reduce ~unwind k e ens t =
+   let svalue =
+     lazy (
+      match t with
+         Cic.Const _ as t -> unwind k e ens t    
+       | t -> reduce (k,e,ens,t,[])
+     ) in
+   let lvalue =
+    lazy (unwind k e ens t)
+   in
+    fun ~reduce ->
+     if reduce then Lazy.force svalue else Lazy.force lvalue
+ end
+;;
+
+module ClosuresOnStackByValueFromEnvOrEnsStrategy =
+ struct
+  type stack_term =
+   int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
+  type env_term = Cic.term
+  type ens_term = Cic.term
+  let to_stack v = (0,[],[],v)
+  let to_stack_list l = List.map to_stack l
+  let to_env v = v
+  let to_ens v = v
+  let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
+  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+  let from_env v = v
+  let from_ens v = v
+  let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
+  let compute_to_env ~reduce ~unwind k e ens t =
+   unwind k e ens t
+  let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
+ end
+;;
+
+module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
+ struct
+  type stack_term =
+   int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
+  type env_term = Cic.term
+  type ens_term = Cic.term
+  let to_stack v = (0,[],[],v)
+  let to_stack_list l = List.map to_stack l
+  let to_env v = v
+  let to_ens v = v
+  let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
+  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
+  let from_env v = v
+  let from_ens v = v
+  let stack_to_env ~reduce ~unwind (k,e,ens,t) =
+   match t with
+      Cic.Const _ as t -> unwind k e ens t    
+    | t -> reduce (k,e,ens,t,[])
+  let compute_to_env ~reduce ~unwind k e ens t =
+   unwind k e ens t
+  let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
+ end
+;;
+
+module Reduction(RS : Strategy) =
+ struct
+  type env = RS.env_term list
+  type ens = RS.ens_term Cic.explicit_named_substitution
+  type stack = RS.stack_term list
+  type config = int * env * ens * Cic.term * stack
+
+  (* k is the length of the environment e *)
+  (* m is the current depth inside the term *)
+  let unwind' m k e ens t = 
+   let module C = Cic in
+   let module S = CicSubstitution in
+    if k = 0 && ens = [] then
+     t
+    else 
+     let rec unwind_aux m =
+      function
+         C.Rel n as t ->
+          if n <= m then t else
+           let d =
+            try
+             Some (RS.from_env (List.nth e (n-m-1)))
+            with _ -> None
+           in
+            (match d with 
+                Some t' ->
+                 if m = 0 then t' else S.lift m t'
+              | None -> C.Rel (n-k)
+            )
+       | C.Var (uri,exp_named_subst) ->
+(*
+prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
+*)
+         if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
+          CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
+         else
+          let params =
+	    let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+           (match o with
+               C.Constant _ -> raise ReferenceToConstant
+             | C.Variable (_,_,_,params,_) -> params
+             | C.CurrentProof _ -> raise ReferenceToCurrentProof
+             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+           )
+          in
+           let exp_named_subst' =
+            substaux_in_exp_named_subst params exp_named_subst m 
+           in
+            C.Var (uri,exp_named_subst')
+       | C.Meta (i,l) ->
+          let l' =
+           List.map
+            (function
+                None -> None
+              | Some t -> Some (unwind_aux m t)
+            ) l
+          in
+           C.Meta (i, l')
+       | C.Sort _ as t -> t
+       | C.Implicit _ as t -> t
+       | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
+       | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
+       | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
+       | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
+       | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
+       | C.Const (uri,exp_named_subst) ->
+          let params =
+	    let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+           (match o with
+               C.Constant (_,_,_,params,_) -> params
+             | C.Variable _ -> raise ReferenceToVariable
+             | C.CurrentProof (_,_,_,_,params,_) -> params
+             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+           )
+          in
+           let exp_named_subst' =
+            substaux_in_exp_named_subst params exp_named_subst m 
+           in
+            C.Const (uri,exp_named_subst')
+       | C.MutInd (uri,i,exp_named_subst) ->
+          let params =
+	    let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+           (match o with
+               C.Constant _ -> raise ReferenceToConstant
+             | C.Variable _ -> raise ReferenceToVariable
+             | C.CurrentProof _ -> raise ReferenceToCurrentProof
+             | C.InductiveDefinition (_,params,_,_) -> params
+           )
+          in
+           let exp_named_subst' =
+            substaux_in_exp_named_subst params exp_named_subst m 
+           in
+            C.MutInd (uri,i,exp_named_subst')
+       | C.MutConstruct (uri,i,j,exp_named_subst) ->
+          let params =
+	    let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+           (match o with
+               C.Constant _ -> raise ReferenceToConstant
+             | C.Variable _ -> raise ReferenceToVariable
+             | C.CurrentProof _ -> raise ReferenceToCurrentProof
+             | C.InductiveDefinition (_,params,_,_) -> params
+           )
+          in
+           let exp_named_subst' =
+            substaux_in_exp_named_subst params exp_named_subst m 
+           in
+            C.MutConstruct (uri,i,j,exp_named_subst')
+       | C.MutCase (sp,i,outt,t,pl) ->
+          C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
+           List.map (unwind_aux m) pl)
+       | C.Fix (i,fl) ->
+          let len = List.length fl in
+          let substitutedfl =
+           List.map
+            (fun (name,i,ty,bo) ->
+              (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
+             fl
+          in
+           C.Fix (i, substitutedfl)
+       | C.CoFix (i,fl) ->
+          let len = List.length fl in
+          let substitutedfl =
+           List.map
+            (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
+             fl
+          in
+           C.CoFix (i, substitutedfl)
+     and substaux_in_exp_named_subst params exp_named_subst' m  =
+  (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
+      let ens' =
+       List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
+  (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
+        List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
+      in
+      let rec filter_and_lift =
+       function
+          [] -> []
+        | uri::tl ->
+           let r = filter_and_lift tl in
+            (try
+              (uri,(List.assq uri ens'))::r
+             with
+              Not_found -> r
+            )
+      in
+       filter_and_lift params
+  *)
+  
+  (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
+  (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
+  
+  (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
+  (*CSC: codice altamente inefficiente *)
+      let rec filter_and_lift already_instantiated =
+       function
+          [] -> []
+        | (uri,t)::tl when
+            List.for_all
+             (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
+            &&
+             not (List.mem uri already_instantiated)
+            &&
+             List.mem uri params
+           ->
+            (uri,CicSubstitution.lift m (RS.from_ens t)) ::
+             (filter_and_lift (uri::already_instantiated) tl)
+        | _::tl -> filter_and_lift already_instantiated tl
+(*
+        | (uri,_)::tl ->
+prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
+prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
+if List.mem uri params then prerr_endline "---- OK2" ;
+        filter_and_lift tl
+*)
+      in
+       List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
+        (filter_and_lift [] (List.rev ens))
+     in
+      unwind_aux m t          
+  ;;
+  
+  let unwind =
+   unwind' 0 
+  ;;
+  
+  let reduce ?(subst = []) context : config -> Cic.term = 
+   let module C = Cic in
+   let module S = CicSubstitution in 
+   let rec reduce =
+    function
+       (k, e, _, (C.Rel n as t), s) ->
+        let d =
+         try
+          Some (RS.from_env (List.nth e (n-1)))
+         with
+          _ ->
+           try
+            begin
+             match List.nth context (n - 1 - k) with
+                None -> assert false
+              | Some (_,C.Decl _) -> None
+              | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
+            end
+           with
+            _ -> None
+        in
+         (match d with 
+             Some t' -> reduce (0,[],[],t',s)
+           | None ->
+              if s = [] then
+               C.Rel (n-k)
+              else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
+         )
+     | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) -> 
+         if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
+          reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
+         else
+          ( let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+            match o with
+              C.Constant _ -> raise ReferenceToConstant
+            | C.CurrentProof _ -> raise ReferenceToCurrentProof
+            | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+            | C.Variable (_,None,_,_,_) ->
+               let t' = unwind k e ens t in
+                if s = [] then t' else
+                 C.Appl (t'::(RS.from_stack_list ~unwind s))
+            | C.Variable (_,Some body,_,_,_) ->
+               let ens' = push_exp_named_subst k e ens exp_named_subst in
+                reduce (0, [], ens', body, s)
+          )
+     | (k, e, ens, (C.Meta (n,l) as t), s) ->
+        (try 
+	   let (_, term,_) = CicUtil.lookup_subst n subst in
+           reduce (k, e, ens,CicSubstitution.subst_meta l term,s)
+	 with  CicUtil.Subst_not_found _ ->
+           let t' = unwind k e ens t in
+           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
+     | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
+     | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
+     | (k, e, ens, (C.Cast (te,ty) as t), s) ->
+        reduce (k, e, ens, te, s) (* s should be empty *)
+     | (k, e, ens, (C.Prod _ as t), s) ->
+         unwind k e ens t (* s should be empty *)
+     | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t' 
+     | (k, e, ens, C.Lambda (_,_,t), p::s) ->
+         reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
+     | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
+        let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
+         reduce (k+1, m'::e, ens, t, s)
+     | (_, _, _, C.Appl [], _) -> assert false
+     | (k, e, ens, C.Appl (he::tl), s) ->
+        let tl' =
+         List.map
+          (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
+        in
+         reduce (k, e, ens, he, (List.append tl') s)
+  (* CSC: Old Dead Code 
+     | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s) 
+     | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)  
+     | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s) 
+     | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
+  (* strict evaluation, but constants are NOT unfolded *)
+        let red =
+         function
+            C.Const _ as t -> unwind k e ens t
+          | t -> reduce (k,e,ens,t,[])
+        in
+         let tl' = List.map red tl in
+          reduce (k, e, ens, he , List.append tl' s)
+     | (k, e, ens, C.Appl l, s) ->
+         C.Appl (List.append (List.map (unwind k e ens) l) s)
+  *)
+     | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
+        (let o,_ = 
+	   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	 in
+	  match o with
+            C.Constant (_,Some body,_,_,_) ->
+             let ens' = push_exp_named_subst k e ens exp_named_subst in
+              (* constants are closed *)
+              reduce (0, [], ens', body, s) 
+          | C.Constant (_,None,_,_,_) ->
+             let t' = unwind k e ens t in
+              if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+          | C.Variable _ -> raise ReferenceToVariable
+          | C.CurrentProof (_,_,body,_,_,_) ->
+             let ens' = push_exp_named_subst k e ens exp_named_subst in
+              (* constants are closed *)
+              reduce (0, [], ens', body, s)
+          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+        )
+     | (k, e, ens, (C.MutInd _ as t),s) ->
+        let t' = unwind k e ens t in 
+         if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+     | (k, e, ens, (C.MutConstruct _ as t),s) -> 
+         let t' = unwind k e ens t in
+          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+     | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
+        let decofix =
+         function
+            C.CoFix (i,fl) as t ->
+             let (_,_,body) = List.nth fl i in
+              let body' =
+               let counter = ref (List.length fl) in
+                List.fold_right
+                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+                 fl
+                 body
+              in
+               (* the term is the result of a reduction; *)
+               (* so it is already unwinded.             *)
+               reduce (0,[],[],body',[])
+          | C.Appl (C.CoFix (i,fl) :: tl) ->
+             let (_,_,body) = List.nth fl i in
+              let body' =
+               let counter = ref (List.length fl) in
+                List.fold_right
+                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+                 fl
+                 body
+              in
+               (* the term is the result of a reduction; *)
+               (* so it is already unwinded.             *)
+               reduce (0,[],[],body',RS.to_stack_list tl)
+          | t -> t
+        in
+         (match decofix (reduce (k,e,ens,term,[])) with
+             C.MutConstruct (_,_,j,_) ->
+              reduce (k, e, ens, (List.nth pl (j-1)), s)
+           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
+              let (arity, r) =
+		let o,_ = 
+		  CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
+		in
+		  match o with
+                      C.InductiveDefinition (tl,ingredients,r,_) ->
+			let (_,_,arity,_) = List.nth tl i in
+			  (arity,r)
+                    | _ -> raise WrongUriToInductiveDefinition
+              in
+               let ts =
+                let num_to_eat = r in
+                 let rec eat_first =
+                  function
+                     (0,l) -> l
+                   | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+                   | _ -> raise (Impossible 5)
+                 in
+                  eat_first (num_to_eat,tl)
+               in
+                (* ts are already unwinded because they are a sublist of tl *)
+                reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
+	   | C.Cast _ | C.Implicit _ ->
+              raise (Impossible 2) (* we don't trust our whd ;-) *)
+           | _ ->
+             let t' = unwind k e ens t in
+              if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+         )
+     | (k, e, ens, (C.Fix (i,fl) as t), s) ->
+        let (_,recindex,_,body) = List.nth fl i in
+         let recparam =
+          try
+           Some (RS.from_stack ~unwind (List.nth s recindex))
+          with
+           _ -> None
+         in
+          (match recparam with
+              Some recparam ->
+               (match reduce (0,[],[],recparam,[]) with
+                   (* match recparam with *) 
+                   C.MutConstruct _
+                 | C.Appl ((C.MutConstruct _)::_) ->
+                    (* OLD 
+                    let body' =
+                     let counter = ref (List.length fl) in
+                      List.fold_right
+                       (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
+                       fl
+                       body
+                    in 
+                     reduce (k, e, ens, body', s) *)
+                    (* NEW *)
+                    let leng = List.length fl in
+                    let fl' = 
+                     let unwind_fl (name,recindex,typ,body) = 
+                      (name,recindex,unwind k e ens typ,
+                        unwind' leng k e ens body)
+                     in
+	              List.map unwind_fl fl
+                    in
+                     let new_env =
+                      let counter = ref 0 in
+                      let rec build_env e =
+                       if !counter = leng then e
+                       else
+                        (incr counter ;
+                         build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
+                      in
+                       build_env e
+                     in
+                      reduce (k+leng, new_env, ens, body, s)  
+                 | _ ->
+                   let t' = unwind k e ens t in 
+                    if s = [] then t' else
+                     C.Appl (t'::(RS.from_stack_list ~unwind s))
+               )
+            | None ->
+               let t' = unwind k e ens t in 
+                if s = [] then t' else
+                 C.Appl (t'::(RS.from_stack_list ~unwind s))
+          )
+     | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
+        let t' = unwind k e ens t in 
+         if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+   and push_exp_named_subst k e ens =
+    function
+       [] -> ens
+     | (uri,t)::tl ->
+         push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
+   in
+     reduce 
+  ;;
+  (*
+  let rec whd context t = 
+    try 
+      reduce context (0, [], [], t, [])
+    with Not_found -> 
+      prerr_endline (CicPp.ppterm t) ; 
+      raise Not_found
+  ;;
+  *)
+
+  let rec whd ?(subst=[]) context t = 
+    reduce ~subst context (0, [], [], t, [])
+  ;;
+
+  
+(* DEBUGGING ONLY
+let whd context t =
+ let res = whd context t in
+ let rescsc = CicReductionNaif.whd context t in
+  if not (CicReductionNaif.are_convertible context res rescsc) then
+   begin
+    prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
+    flush stderr ;
+    prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
+    flush stderr ;
+    prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
+    flush stderr ;
+CicReductionNaif.fdebug := 0 ;
+let _ =  CicReductionNaif.are_convertible context res rescsc in
+    assert false ;
+   end
+  else 
+   res
+;;
+*)
+ end
+;;
+
+
+(*
+module R = Reduction CallByNameStrategy;;
+module R = Reduction CallByValueStrategy;;
+module R = Reduction CallByValueStrategyByNameOnConstants;;
+module R = Reduction LazyCallByValueStrategy;;
+module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
+module R = Reduction LazyCallByNameStrategy;;
+module R = Reduction
+ LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
+module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
+module R = Reduction
+ ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
+*)
+module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module U = UriManager;;
+
+let whd = R.whd;;
+
+  (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
+    * fallbacks to structural equality *)
+let (===) x y = (Pervasives.compare x y = 0)
+
+(* t1, t2 must be well-typed *)
+let are_convertible ?(subst=[]) ?(metasenv=[])  =
+ let rec aux test_equality_only context t1 t2 ugraph =
+  let aux2 test_equality_only t1 t2 ugraph =
+
+   (* this trivial euristic cuts down the total time of about five times ;-) *)
+   (* this because most of the time t1 and t2 are "sintactically" the same   *)
+   if t1 === t2 then
+     true,ugraph
+   else
+    begin
+     let module C = Cic in
+       match (t1,t2) with
+          (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
+        | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
+            if U.eq uri1 uri2 then
+             (try
+               List.fold_right2
+                (fun (uri1,x) (uri2,y) (b,ugraph) ->
+                  let b',ugraph' = aux test_equality_only context x y ugraph in
+                  (U.eq uri1 uri2 && b' && b),ugraph'
+                ) exp_named_subst1 exp_named_subst2 (true,ugraph) 
+              with
+               Invalid_argument _ -> false,ugraph
+             )
+	    else
+	      false,ugraph
+        | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
+	    if n1 = n2 then
+	      let b2, ugraph1 = 
+		let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
+		let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
+		  List.fold_left2
+		    (fun (b,ugraph) t1 t2 ->
+		       if b then 
+			 match t1,t2 with
+			     None,_
+			   | _,None  -> true,ugraph
+			   | Some t1',Some t2' -> 
+			       aux test_equality_only context t1' t2' ugraph
+		       else
+			 false,ugraph
+		    ) (true,ugraph) l1 l2
+	      in
+		if b2 then true,ugraph1 else false,ugraph 
+	    else
+	      false,ugraph
+          (* TASSI: CONSTRAINTS *)
+	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+	    true,(CicUniv.add_eq t2 t1 ugraph)
+	  (* TASSI: CONSTRAINTS *)
+	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+	    true,(CicUniv.add_ge t2 t1 ugraph)
+	  (* TASSI: CONSTRAINTS *)
+	| (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
+	  (* TASSI: CONSTRAINTS *)
+        | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
+        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+	    let b',ugraph' = aux true context s1 s2 ugraph in
+	    if b' then 
+              aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
+		t1 t2 ugraph'
+	    else
+	      false,ugraph
+        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
+           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
+           if b' then
+	     aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
+	       t1 t2 ugraph'
+	   else
+	     false,ugraph
+        | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
+           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
+	   if b' then
+            aux test_equality_only
+             ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
+	   else
+	     false,ugraph
+        | (C.Appl l1, C.Appl l2) ->
+           (try
+             List.fold_right2
+               (fun  x y (b,ugraph) -> 
+		 if b then
+		   aux test_equality_only context x y ugraph
+	         else
+	           false,ugraph) l1 l2 (true,ugraph)
+            with
+             Invalid_argument _ -> false,ugraph
+           )
+        | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
+            let b' = U.eq uri1 uri2 in
+	    if b' then
+             (try
+               List.fold_right2
+                (fun (uri1,x) (uri2,y) (b,ugraph) ->
+		  if b && U.eq uri1 uri2 then
+		    aux test_equality_only context x y ugraph 
+		  else
+		    false,ugraph
+                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
+              with
+               Invalid_argument _ -> false,ugraph
+             )
+	    else
+	      false,ugraph
+        | (C.MutInd (uri1,i1,exp_named_subst1),
+           C.MutInd (uri2,i2,exp_named_subst2)
+          ) ->
+            let b' = U.eq uri1 uri2 && i1 = i2 in
+	    if b' then
+             (try
+               List.fold_right2
+                (fun (uri1,x) (uri2,y) (b,ugraph) ->
+                  if b && U.eq uri1 uri2 then
+		    aux test_equality_only context x y ugraph
+		  else
+		   false,ugraph
+                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
+              with
+               Invalid_argument _ -> false,ugraph
+             )
+	    else 
+	      false,ugraph
+        | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
+           C.MutConstruct (uri2,i2,j2,exp_named_subst2)
+          ) ->
+            let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
+	    if b' then
+             (try
+               List.fold_right2
+                (fun (uri1,x) (uri2,y) (b,ugraph) ->
+		  if b && U.eq uri1 uri2 then
+		    aux test_equality_only context x y ugraph
+		  else
+		    false,ugraph
+                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
+              with
+               Invalid_argument _ -> false,ugraph
+             )
+	    else
+	      false,ugraph
+        | (C.MutCase (uri1,i1,outtype1,term1,pl1),
+           C.MutCase (uri2,i2,outtype2,term2,pl2)) -> 
+            let b' = U.eq uri1 uri2 && i1 = i2 in
+	    if b' then
+             let b'',ugraph''=aux test_equality_only context 
+		 outtype1 outtype2 ugraph in
+	     if b'' then 
+	       let b''',ugraph'''= aux test_equality_only context 
+		   term1 term2 ugraph'' in
+	       List.fold_right2
+		 (fun x y (b,ugraph) -> 
+		   if b then
+		     aux test_equality_only context x y ugraph 
+		   else 
+		     false,ugraph)
+		 pl1 pl2 (true,ugraph''')
+	     else
+	       false,ugraph
+	    else
+	      false,ugraph
+        | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
+            let tys =
+              List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+            in
+            if i1 = i2 then
+             List.fold_right2
+              (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
+                if b && recindex1 = recindex2 then
+		  let b',ugraph' = aux test_equality_only context ty1 ty2 
+		      ugraph in
+		  if b' then
+		    aux test_equality_only (tys@context) bo1 bo2 ugraph'
+	          else
+	            false,ugraph
+	        else
+	          false,ugraph)
+	     fl1 fl2 (true,ugraph)
+	    else
+	      false,ugraph
+        | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
+           let tys =
+            List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+           in
+            if i1 = i2 then
+              List.fold_right2
+              (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
+		if b then
+		  let b',ugraph' = aux test_equality_only context ty1 ty2 
+		      ugraph in
+		  if b' then
+		    aux test_equality_only (tys@context) bo1 bo2 ugraph'
+	          else
+	            false,ugraph
+	        else
+	          false,ugraph)
+	     fl1 fl2 (true,ugraph)
+	    else
+	      false,ugraph
+        | (C.Cast _, _) | (_, C.Cast _)
+        | (C.Implicit _, _) | (_, C.Implicit _) ->
+            assert false
+        | (_,_) -> false,ugraph
+    end
+  in
+     begin
+     debug t1 [t2] "PREWHD";
+     (* 
+     (match t1 with 
+	 Cic.Meta _ -> 
+	   prerr_endline (CicPp.ppterm t1);
+	   prerr_endline (CicPp.ppterm (whd ~subst context t1));
+	   prerr_endline (CicPp.ppterm t2);
+	   prerr_endline (CicPp.ppterm (whd ~subst context t2))
+       | _ -> ()); *)
+     let t1' = whd ~subst context t1 in
+     let t2' = whd ~subst context t2 in
+      debug t1' [t2'] "POSTWHD";
+      aux2 test_equality_only t1' t2' ugraph
+    end
+ in
+  aux false (*c t1 t2 ugraph *)
+;;
+
diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
deleted file mode 100644
index 0610504c4..000000000
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ /dev/null
@@ -1,1036 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* TODO unify exceptions *)
-
-exception CicReductionInternalError;;
-exception WrongUriToInductiveDefinition;;
-exception Impossible of int;;
-exception ReferenceToConstant;;
-exception ReferenceToVariable;;
-exception ReferenceToCurrentProof;;
-exception ReferenceToInductiveDefinition;;
-
-let fdebug = ref 1;;
-let debug t env s =
- let rec debug_aux t i =
-  let module C = Cic in
-  let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
- in
-  if !fdebug = 0 then
-   prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
-;;
-
-module type Strategy =
- sig
-  type stack_term
-  type env_term
-  type ens_term
-  val to_stack : Cic.term -> stack_term
-  val to_stack_list : Cic.term list -> stack_term list
-  val to_env : Cic.term -> env_term
-  val to_ens : Cic.term -> ens_term
-  val from_stack :
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
-   stack_term -> Cic.term
-  val from_stack_list :
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
-   stack_term list -> Cic.term list
-  val from_env : env_term -> Cic.term
-  val from_ens : ens_term -> Cic.term
-  val stack_to_env :
-   reduce:
-    (int * env_term list * ens_term Cic.explicit_named_substitution *
-      Cic.term * stack_term list -> Cic.term) ->
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
-   stack_term -> env_term
-  val compute_to_env :
-   reduce:
-    (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
-      stack_term list -> Cic.term) ->
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
-   int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-    Cic.term -> env_term
-  val compute_to_stack :
-   reduce:
-    (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
-      stack_term list -> Cic.term) ->
-   unwind:
-    (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-      Cic.term -> Cic.term) ->
-   int -> env_term list -> ens_term Cic.explicit_named_substitution ->
-    Cic.term -> stack_term
- end
-;;
-
-module CallByNameStrategy =
- struct
-  type stack_term = Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  let to_stack v = v
-  let to_stack_list l = l
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind v = v
-  let from_stack_list ~unwind l = l
-  let from_env v = v
-  let from_ens v = v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
-  let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
- end
-;;
-
-module CallByValueStrategy =
- struct
-  type stack_term = Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  let to_stack v = v
-  let to_stack_list l = l
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind v = v
-  let from_stack_list ~unwind l = l
-  let from_env v = v
-  let from_ens v = v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
-  let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
- end
-;;
-
-module CallByValueStrategyByNameOnConstants =
- struct
-  type stack_term = Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  let to_stack v = v
-  let to_stack_list l = l
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind v = v
-  let from_stack_list ~unwind l = l
-  let from_env v = v
-  let from_ens v = v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens =
-   function
-      Cic.Const _ as t -> unwind k e ens t    
-    | t -> reduce (k,e,ens,t,[])
-  let compute_to_env ~reduce ~unwind k e ens =
-   function
-      Cic.Const _ as t -> unwind k e ens t    
-    | t -> reduce (k,e,ens,t,[])
- end
-;;
-
-module LazyCallByValueStrategy =
- struct
-  type stack_term = Cic.term lazy_t
-  type env_term = Cic.term lazy_t
-  type ens_term = Cic.term lazy_t
-  let to_stack v = lazy v
-  let to_stack_list l = List.map to_stack l
-  let to_env v = lazy v
-  let to_ens v = lazy v
-  let from_stack ~unwind v = Lazy.force v
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = Lazy.force v
-  let from_ens v = Lazy.force v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
-  let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
- end
-;;
-
-module LazyCallByValueStrategyByNameOnConstants =
- struct
-  type stack_term = Cic.term lazy_t
-  type env_term = Cic.term lazy_t
-  type ens_term = Cic.term lazy_t
-  let to_stack v = lazy v
-  let to_stack_list l = List.map to_stack l
-  let to_env v = lazy v
-  let to_ens v = lazy v
-  let from_stack ~unwind v = Lazy.force v
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = Lazy.force v
-  let from_ens v = Lazy.force v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t =
-   lazy (
-    match t with
-       Cic.Const _ as t -> unwind k e ens t    
-     | t -> reduce (k,e,ens,t,[]))
-  let compute_to_env ~reduce ~unwind k e ens t =
-   lazy (
-    match t with
-       Cic.Const _ as t -> unwind k e ens t    
-     | t -> reduce (k,e,ens,t,[]))
- end
-;;
-
-module LazyCallByNameStrategy =
- struct
-  type stack_term = Cic.term lazy_t
-  type env_term = Cic.term lazy_t
-  type ens_term = Cic.term lazy_t
-  let to_stack v = lazy v
-  let to_stack_list l = List.map to_stack l
-  let to_env v = lazy v
-  let to_ens v = lazy v
-  let from_stack ~unwind v = Lazy.force v
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = Lazy.force v
-  let from_ens v = Lazy.force v
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
-  let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
- end
-;;
-
-module
- LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
-=
- struct
-  type stack_term = reduce:bool -> Cic.term
-  type env_term = reduce:bool -> Cic.term
-  type ens_term = reduce:bool -> Cic.term
-  let to_stack v =
-   let value = lazy v in
-    fun ~reduce -> Lazy.force value
-  let to_stack_list l = List.map to_stack l
-  let to_env v =
-   let value = lazy v in
-    fun ~reduce -> Lazy.force value
-  let to_ens v =
-   let value = lazy v in
-    fun ~reduce -> Lazy.force value
-  let from_stack ~unwind v = (v ~reduce:false)
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = (v ~reduce:true)
-  let from_ens v = (v ~reduce:true)
-  let stack_to_env ~reduce ~unwind v = v
-  let compute_to_stack ~reduce ~unwind k e ens t =
-   let svalue =
-     lazy (
-      match t with
-         Cic.Const _ as t -> unwind k e ens t    
-       | t -> reduce (k,e,ens,t,[])
-     ) in
-   let lvalue =
-    lazy (unwind k e ens t)
-   in
-    fun ~reduce ->
-     if reduce then Lazy.force svalue else Lazy.force lvalue
-  let compute_to_env ~reduce ~unwind k e ens t =
-   let svalue =
-     lazy (
-      match t with
-         Cic.Const _ as t -> unwind k e ens t    
-       | t -> reduce (k,e,ens,t,[])
-     ) in
-   let lvalue =
-    lazy (unwind k e ens t)
-   in
-    fun ~reduce ->
-     if reduce then Lazy.force svalue else Lazy.force lvalue
- end
-;;
-
-module ClosuresOnStackByValueFromEnvOrEnsStrategy =
- struct
-  type stack_term =
-   int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  let to_stack v = (0,[],[],v)
-  let to_stack_list l = List.map to_stack l
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = v
-  let from_ens v = v
-  let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
-  let compute_to_env ~reduce ~unwind k e ens t =
-   unwind k e ens t
-  let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
- end
-;;
-
-module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
- struct
-  type stack_term =
-   int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
-  type env_term = Cic.term
-  type ens_term = Cic.term
-  let to_stack v = (0,[],[],v)
-  let to_stack_list l = List.map to_stack l
-  let to_env v = v
-  let to_ens v = v
-  let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
-  let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
-  let from_env v = v
-  let from_ens v = v
-  let stack_to_env ~reduce ~unwind (k,e,ens,t) =
-   match t with
-      Cic.Const _ as t -> unwind k e ens t    
-    | t -> reduce (k,e,ens,t,[])
-  let compute_to_env ~reduce ~unwind k e ens t =
-   unwind k e ens t
-  let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
- end
-;;
-
-module Reduction(RS : Strategy) =
- struct
-  type env = RS.env_term list
-  type ens = RS.ens_term Cic.explicit_named_substitution
-  type stack = RS.stack_term list
-  type config = int * env * ens * Cic.term * stack
-
-  (* k is the length of the environment e *)
-  (* m is the current depth inside the term *)
-  let unwind' m k e ens t = 
-   let module C = Cic in
-   let module S = CicSubstitution in
-    if k = 0 && ens = [] then
-     t
-    else 
-     let rec unwind_aux m =
-      function
-         C.Rel n as t ->
-          if n <= m then t else
-           let d =
-            try
-             Some (RS.from_env (List.nth e (n-m-1)))
-            with _ -> None
-           in
-            (match d with 
-                Some t' ->
-                 if m = 0 then t' else S.lift m t'
-              | None -> C.Rel (n-k)
-            )
-       | C.Var (uri,exp_named_subst) ->
-(*
-prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
-*)
-         if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
-          CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
-         else
-          let params =
-	    let o,_ = 
-	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-	    in
-           (match o with
-               C.Constant _ -> raise ReferenceToConstant
-             | C.Variable (_,_,_,params,_) -> params
-             | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-           )
-          in
-           let exp_named_subst' =
-            substaux_in_exp_named_subst params exp_named_subst m 
-           in
-            C.Var (uri,exp_named_subst')
-       | C.Meta (i,l) ->
-          let l' =
-           List.map
-            (function
-                None -> None
-              | Some t -> Some (unwind_aux m t)
-            ) l
-          in
-           C.Meta (i, l')
-       | C.Sort _ as t -> t
-       | C.Implicit _ as t -> t
-       | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
-       | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
-       | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
-       | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
-       | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
-       | C.Const (uri,exp_named_subst) ->
-          let params =
-	    let o,_ = 
-	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-	    in
-           (match o with
-               C.Constant (_,_,_,params,_) -> params
-             | C.Variable _ -> raise ReferenceToVariable
-             | C.CurrentProof (_,_,_,_,params,_) -> params
-             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-           )
-          in
-           let exp_named_subst' =
-            substaux_in_exp_named_subst params exp_named_subst m 
-           in
-            C.Const (uri,exp_named_subst')
-       | C.MutInd (uri,i,exp_named_subst) ->
-          let params =
-	    let o,_ = 
-	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-	    in
-           (match o with
-               C.Constant _ -> raise ReferenceToConstant
-             | C.Variable _ -> raise ReferenceToVariable
-             | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_,_) -> params
-           )
-          in
-           let exp_named_subst' =
-            substaux_in_exp_named_subst params exp_named_subst m 
-           in
-            C.MutInd (uri,i,exp_named_subst')
-       | C.MutConstruct (uri,i,j,exp_named_subst) ->
-          let params =
-	    let o,_ = 
-	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-	    in
-           (match o with
-               C.Constant _ -> raise ReferenceToConstant
-             | C.Variable _ -> raise ReferenceToVariable
-             | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_,_) -> params
-           )
-          in
-           let exp_named_subst' =
-            substaux_in_exp_named_subst params exp_named_subst m 
-           in
-            C.MutConstruct (uri,i,j,exp_named_subst')
-       | C.MutCase (sp,i,outt,t,pl) ->
-          C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
-           List.map (unwind_aux m) pl)
-       | C.Fix (i,fl) ->
-          let len = List.length fl in
-          let substitutedfl =
-           List.map
-            (fun (name,i,ty,bo) ->
-              (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
-             fl
-          in
-           C.Fix (i, substitutedfl)
-       | C.CoFix (i,fl) ->
-          let len = List.length fl in
-          let substitutedfl =
-           List.map
-            (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
-             fl
-          in
-           C.CoFix (i, substitutedfl)
-     and substaux_in_exp_named_subst params exp_named_subst' m  =
-  (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
-      let ens' =
-       List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
-  (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
-        List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
-      in
-      let rec filter_and_lift =
-       function
-          [] -> []
-        | uri::tl ->
-           let r = filter_and_lift tl in
-            (try
-              (uri,(List.assq uri ens'))::r
-             with
-              Not_found -> r
-            )
-      in
-       filter_and_lift params
-  *)
-  
-  (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
-  (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
-  
-  (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
-  (*CSC: codice altamente inefficiente *)
-      let rec filter_and_lift already_instantiated =
-       function
-          [] -> []
-        | (uri,t)::tl when
-            List.for_all
-             (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
-            &&
-             not (List.mem uri already_instantiated)
-            &&
-             List.mem uri params
-           ->
-            (uri,CicSubstitution.lift m (RS.from_ens t)) ::
-             (filter_and_lift (uri::already_instantiated) tl)
-        | _::tl -> filter_and_lift already_instantiated tl
-(*
-        | (uri,_)::tl ->
-prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
-if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
-prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then prerr_endline "---- OK2" ;
-        filter_and_lift tl
-*)
-      in
-       List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
-        (filter_and_lift [] (List.rev ens))
-     in
-      unwind_aux m t          
-  ;;
-  
-  let unwind =
-   unwind' 0 
-  ;;
-  
-  let reduce ?(subst = []) context : config -> Cic.term = 
-   let module C = Cic in
-   let module S = CicSubstitution in 
-   let rec reduce =
-    function
-       (k, e, _, (C.Rel n as t), s) ->
-        let d =
-         try
-          Some (RS.from_env (List.nth e (n-1)))
-         with
-          _ ->
-           try
-            begin
-             match List.nth context (n - 1 - k) with
-                None -> assert false
-              | Some (_,C.Decl _) -> None
-              | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
-            end
-           with
-            _ -> None
-        in
-         (match d with 
-             Some t' -> reduce (0,[],[],t',s)
-           | None ->
-              if s = [] then
-               C.Rel (n-k)
-              else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
-         )
-     | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) -> 
-         if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
-          reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
-         else
-          ( let o,_ = 
-	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-	    in
-            match o with
-              C.Constant _ -> raise ReferenceToConstant
-            | C.CurrentProof _ -> raise ReferenceToCurrentProof
-            | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-            | C.Variable (_,None,_,_,_) ->
-               let t' = unwind k e ens t in
-                if s = [] then t' else
-                 C.Appl (t'::(RS.from_stack_list ~unwind s))
-            | C.Variable (_,Some body,_,_,_) ->
-               let ens' = push_exp_named_subst k e ens exp_named_subst in
-                reduce (0, [], ens', body, s)
-          )
-     | (k, e, ens, (C.Meta (n,l) as t), s) ->
-        (try 
-	   let (_, term,_) = CicUtil.lookup_subst n subst in
-           reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
-	 with  CicUtil.Subst_not_found _ ->
-           let t' = unwind k e ens t in
-           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
-     | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
-     | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
-     | (k, e, ens, (C.Cast (te,ty) as t), s) ->
-        reduce (k, e, ens, te, s) (* s should be empty *)
-     | (k, e, ens, (C.Prod _ as t), s) ->
-         unwind k e ens t (* s should be empty *)
-     | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t' 
-     | (k, e, ens, C.Lambda (_,_,t), p::s) ->
-         reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
-     | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
-        let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
-         reduce (k+1, m'::e, ens, t, s)
-     | (_, _, _, C.Appl [], _) -> assert false
-     | (k, e, ens, C.Appl (he::tl), s) ->
-        let tl' =
-         List.map
-          (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
-        in
-         reduce (k, e, ens, he, (List.append tl') s)
-  (* CSC: Old Dead Code 
-     | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s) 
-     | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)  
-     | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s) 
-     | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
-  (* strict evaluation, but constants are NOT unfolded *)
-        let red =
-         function
-            C.Const _ as t -> unwind k e ens t
-          | t -> reduce (k,e,ens,t,[])
-        in
-         let tl' = List.map red tl in
-          reduce (k, e, ens, he , List.append tl' s)
-     | (k, e, ens, C.Appl l, s) ->
-         C.Appl (List.append (List.map (unwind k e ens) l) s)
-  *)
-     | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
-        (let o,_ = 
-	   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-	 in
-	  match o with
-            C.Constant (_,Some body,_,_,_) ->
-             let ens' = push_exp_named_subst k e ens exp_named_subst in
-              (* constants are closed *)
-              reduce (0, [], ens', body, s) 
-          | C.Constant (_,None,_,_,_) ->
-             let t' = unwind k e ens t in
-              if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
-          | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,body,_,_,_) ->
-             let ens' = push_exp_named_subst k e ens exp_named_subst in
-              (* constants are closed *)
-              reduce (0, [], ens', body, s)
-          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-        )
-     | (k, e, ens, (C.MutInd _ as t),s) ->
-        let t' = unwind k e ens t in 
-         if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
-     | (k, e, ens, (C.MutConstruct _ as t),s) -> 
-         let t' = unwind k e ens t in
-          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
-     | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
-        let decofix =
-         function
-            C.CoFix (i,fl) as t ->
-             let (_,_,body) = List.nth fl i in
-              let body' =
-               let counter = ref (List.length fl) in
-                List.fold_right
-                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                 fl
-                 body
-              in
-               (* the term is the result of a reduction; *)
-               (* so it is already unwinded.             *)
-               reduce (0,[],[],body',[])
-          | C.Appl (C.CoFix (i,fl) :: tl) ->
-             let (_,_,body) = List.nth fl i in
-              let body' =
-               let counter = ref (List.length fl) in
-                List.fold_right
-                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                 fl
-                 body
-              in
-               (* the term is the result of a reduction; *)
-               (* so it is already unwinded.             *)
-               reduce (0,[],[],body',RS.to_stack_list tl)
-          | t -> t
-        in
-         (match decofix (reduce (k,e,ens,term,[])) with
-             C.MutConstruct (_,_,j,_) ->
-              reduce (k, e, ens, (List.nth pl (j-1)), s)
-           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
-              let (arity, r) =
-		let o,_ = 
-		  CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
-		in
-		  match o with
-                      C.InductiveDefinition (tl,ingredients,r,_) ->
-			let (_,_,arity,_) = List.nth tl i in
-			  (arity,r)
-                    | _ -> raise WrongUriToInductiveDefinition
-              in
-               let ts =
-                let num_to_eat = r in
-                 let rec eat_first =
-                  function
-                     (0,l) -> l
-                   | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
-                   | _ -> raise (Impossible 5)
-                 in
-                  eat_first (num_to_eat,tl)
-               in
-                (* ts are already unwinded because they are a sublist of tl *)
-                reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
-	   | C.Cast _ | C.Implicit _ ->
-              raise (Impossible 2) (* we don't trust our whd ;-) *)
-           | _ ->
-             let t' = unwind k e ens t in
-              if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
-         )
-     | (k, e, ens, (C.Fix (i,fl) as t), s) ->
-        let (_,recindex,_,body) = List.nth fl i in
-         let recparam =
-          try
-           Some (RS.from_stack ~unwind (List.nth s recindex))
-          with
-           _ -> None
-         in
-          (match recparam with
-              Some recparam ->
-               (match reduce (0,[],[],recparam,[]) with
-                   (* match recparam with *) 
-                   C.MutConstruct _
-                 | C.Appl ((C.MutConstruct _)::_) ->
-                    (* OLD 
-                    let body' =
-                     let counter = ref (List.length fl) in
-                      List.fold_right
-                       (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
-                       fl
-                       body
-                    in 
-                     reduce (k, e, ens, body', s) *)
-                    (* NEW *)
-                    let leng = List.length fl in
-                    let fl' = 
-                     let unwind_fl (name,recindex,typ,body) = 
-                      (name,recindex,unwind k e ens typ,
-                        unwind' leng k e ens body)
-                     in
-	              List.map unwind_fl fl
-                    in
-                     let new_env =
-                      let counter = ref 0 in
-                      let rec build_env e =
-                       if !counter = leng then e
-                       else
-                        (incr counter ;
-                         build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
-                      in
-                       build_env e
-                     in
-                      reduce (k+leng, new_env, ens, body, s)  
-                 | _ ->
-                   let t' = unwind k e ens t in 
-                    if s = [] then t' else
-                     C.Appl (t'::(RS.from_stack_list ~unwind s))
-               )
-            | None ->
-               let t' = unwind k e ens t in 
-                if s = [] then t' else
-                 C.Appl (t'::(RS.from_stack_list ~unwind s))
-          )
-     | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
-        let t' = unwind k e ens t in 
-         if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
-   and push_exp_named_subst k e ens =
-    function
-       [] -> ens
-     | (uri,t)::tl ->
-         push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
-   in
-     reduce 
-  ;;
-  (*
-  let rec whd context t = 
-    try 
-      reduce context (0, [], [], t, [])
-    with Not_found -> 
-      prerr_endline (CicPp.ppterm t) ; 
-      raise Not_found
-  ;;
-  *)
-
-  let rec whd ?(subst=[]) context t = 
-    reduce ~subst context (0, [], [], t, [])
-  ;;
-
-  
-(* DEBUGGING ONLY
-let whd context t =
- let res = whd context t in
- let rescsc = CicReductionNaif.whd context t in
-  if not (CicReductionNaif.are_convertible context res rescsc) then
-   begin
-    prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
-    flush stderr ;
-    prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
-    flush stderr ;
-    prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
-    flush stderr ;
-CicReductionNaif.fdebug := 0 ;
-let _ =  CicReductionNaif.are_convertible context res rescsc in
-    assert false ;
-   end
-  else 
-   res
-;;
-*)
- end
-;;
-
-
-(*
-module R = Reduction CallByNameStrategy;;
-module R = Reduction CallByValueStrategy;;
-module R = Reduction CallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByValueStrategy;;
-module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByNameStrategy;;
-module R = Reduction
- LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
-module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
-module R = Reduction
- ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
-*)
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
-module U = UriManager;;
-
-let whd = R.whd;;
-
-  (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
-    * fallbacks to structural equality *)
-let (===) x y = (Pervasives.compare x y = 0)
-
-(* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) ?(metasenv=[])  =
- let rec aux test_equality_only context t1 t2 ugraph =
-  let aux2 test_equality_only t1 t2 ugraph =
-
-   (* this trivial euristic cuts down the total time of about five times ;-) *)
-   (* this because most of the time t1 and t2 are "sintactically" the same   *)
-   if t1 === t2 then
-     true,ugraph
-   else
-    begin
-     let module C = Cic in
-       match (t1,t2) with
-          (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
-        | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
-            if U.eq uri1 uri2 then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-                  let b',ugraph' = aux test_equality_only context x y ugraph in
-                  (U.eq uri1 uri2 && b' && b),ugraph'
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph) 
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-	    else
-	      false,ugraph
-        | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
-	    if n1 = n2 then
-	      let b2, ugraph1 = 
-		let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
-		let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
-		  List.fold_left2
-		    (fun (b,ugraph) t1 t2 ->
-		       if b then 
-			 match t1,t2 with
-			     None,_
-			   | _,None  -> true,ugraph
-			   | Some t1',Some t2' -> 
-			       aux test_equality_only context t1' t2' ugraph
-		       else
-			 false,ugraph
-		    ) (true,ugraph) l1 l2
-	      in
-		if b2 then true,ugraph1 else false,ugraph 
-	    else
-	      false,ugraph
-          (* TASSI: CONSTRAINTS *)
-	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
-	    true,(CicUniv.add_eq t2 t1 ugraph)
-	  (* TASSI: CONSTRAINTS *)
-	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
-	    true,(CicUniv.add_ge t2 t1 ugraph)
-	  (* TASSI: CONSTRAINTS *)
-	| (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
-	  (* TASSI: CONSTRAINTS *)
-        | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
-        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-	    let b',ugraph' = aux true context s1 s2 ugraph in
-	    if b' then 
-              aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
-		t1 t2 ugraph'
-	    else
-	      false,ugraph
-        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
-           if b' then
-	     aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
-	       t1 t2 ugraph'
-	   else
-	     false,ugraph
-        | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
-           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
-	   if b' then
-            aux test_equality_only
-             ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
-	   else
-	     false,ugraph
-        | (C.Appl l1, C.Appl l2) ->
-           (try
-             List.fold_right2
-               (fun  x y (b,ugraph) -> 
-		 if b then
-		   aux test_equality_only context x y ugraph
-	         else
-	           false,ugraph) l1 l2 (true,ugraph)
-            with
-             Invalid_argument _ -> false,ugraph
-           )
-        | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
-            let b' = U.eq uri1 uri2 in
-	    if b' then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-		  if b && U.eq uri1 uri2 then
-		    aux test_equality_only context x y ugraph 
-		  else
-		    false,ugraph
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-	    else
-	      false,ugraph
-        | (C.MutInd (uri1,i1,exp_named_subst1),
-           C.MutInd (uri2,i2,exp_named_subst2)
-          ) ->
-            let b' = U.eq uri1 uri2 && i1 = i2 in
-	    if b' then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-                  if b && U.eq uri1 uri2 then
-		    aux test_equality_only context x y ugraph
-		  else
-		   false,ugraph
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-	    else 
-	      false,ugraph
-        | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
-           C.MutConstruct (uri2,i2,j2,exp_named_subst2)
-          ) ->
-            let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
-	    if b' then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-		  if b && U.eq uri1 uri2 then
-		    aux test_equality_only context x y ugraph
-		  else
-		    false,ugraph
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-	    else
-	      false,ugraph
-        | (C.MutCase (uri1,i1,outtype1,term1,pl1),
-           C.MutCase (uri2,i2,outtype2,term2,pl2)) -> 
-            let b' = U.eq uri1 uri2 && i1 = i2 in
-	    if b' then
-             let b'',ugraph''=aux test_equality_only context 
-		 outtype1 outtype2 ugraph in
-	     if b'' then 
-	       let b''',ugraph'''= aux test_equality_only context 
-		   term1 term2 ugraph'' in
-	       List.fold_right2
-		 (fun x y (b,ugraph) -> 
-		   if b then
-		     aux test_equality_only context x y ugraph 
-		   else 
-		     false,ugraph)
-		 pl1 pl2 (true,ugraph''')
-	     else
-	       false,ugraph
-	    else
-	      false,ugraph
-        | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-            let tys =
-              List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
-            in
-            if i1 = i2 then
-             List.fold_right2
-              (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
-                if b && recindex1 = recindex2 then
-		  let b',ugraph' = aux test_equality_only context ty1 ty2 
-		      ugraph in
-		  if b' then
-		    aux test_equality_only (tys@context) bo1 bo2 ugraph'
-	          else
-	            false,ugraph
-	        else
-	          false,ugraph)
-	     fl1 fl2 (true,ugraph)
-	    else
-	      false,ugraph
-        | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-           let tys =
-            List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
-           in
-            if i1 = i2 then
-              List.fold_right2
-              (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
-		if b then
-		  let b',ugraph' = aux test_equality_only context ty1 ty2 
-		      ugraph in
-		  if b' then
-		    aux test_equality_only (tys@context) bo1 bo2 ugraph'
-	          else
-	            false,ugraph
-	        else
-	          false,ugraph)
-	     fl1 fl2 (true,ugraph)
-	    else
-	      false,ugraph
-        | (C.Cast _, _) | (_, C.Cast _)
-        | (C.Implicit _, _) | (_, C.Implicit _) ->
-            assert false
-        | (_,_) -> false,ugraph
-    end
-  in
-     begin
-     debug t1 [t2] "PREWHD";
-     (* 
-     (match t1 with 
-	 Cic.Meta _ -> 
-	   prerr_endline (CicPp.ppterm t1);
-	   prerr_endline (CicPp.ppterm (whd ~subst context t1));
-	   prerr_endline (CicPp.ppterm t2);
-	   prerr_endline (CicPp.ppterm (whd ~subst context t2))
-       | _ -> ()); *)
-     let t1' = whd ~subst context t1 in
-     let t2' = whd ~subst context t2 in
-      debug t1' [t2'] "POSTWHD";
-      aux2 test_equality_only t1' t2' ugraph
-    end
- in
-  aux false (*c t1 t2 ugraph *)
-;;
-
diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.mli b/helm/ocaml/cic_proof_checking/cicReductionMachine.mli
deleted file mode 100644
index 7e36a05d2..000000000
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-exception WrongUriToInductiveDefinition
-exception ReferenceToConstant
-exception ReferenceToVariable
-exception ReferenceToCurrentProof
-exception ReferenceToInductiveDefinition
-val fdebug : int ref
-val whd : Cic.context -> Cic.term -> Cic.term
-val are_convertible : Cic.context -> Cic.term -> Cic.term -> CicUniv.universe_graph ->  bool * CicUniv.universe_graph
diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
deleted file mode 100644
index 04067ccbf..000000000
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ /dev/null
@@ -1,407 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-exception CicReductionInternalError;;
-exception WrongUriToInductiveDefinition;;
-
-let fdebug = ref 1;;
-let debug t env s =
- let rec debug_aux t i =
-  let module C = Cic in
-  let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
- in
-  if !fdebug = 0 then
-   prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
-;;
-
-exception Impossible of int;;
-exception ReferenceToConstant;;
-exception ReferenceToVariable;;
-exception ReferenceToCurrentProof;;
-exception ReferenceToInductiveDefinition;;
-exception RelToHiddenHypothesis;;
-
-(* takes a well-typed term *)
-let whd context =
- let rec whdaux l =
-  let module C = Cic in
-  let module S = CicSubstitution in
-   function
-      C.Rel n as t ->
-       (match List.nth context (n-1) with
-           Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_, C.Def (bo,_)) -> whdaux l (S.lift n bo)
-	  | None -> raise RelToHiddenHypothesis
-       )
-    | C.Var (uri,exp_named_subst) as t ->
-	let o,_ = 
-	  CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
-	in
-       (match o with
-           C.Constant _ -> raise ReferenceToConstant
-         | C.CurrentProof _ -> raise ReferenceToCurrentProof
-         | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-         | C.Variable (_,None,_,_,_) -> if l = [] then t else C.Appl (t::l)
-         | C.Variable (_,Some body,_,_,_) ->
-            whdaux l (CicSubstitution.subst_vars exp_named_subst body)
-       )
-    | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
-    | C.Sort _ as t -> t (* l should be empty *)
-    | C.Implicit _ as t -> t
-    | C.Cast (te,ty) -> whdaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
-    | C.Prod _ as t -> t (* l should be empty *)
-    | C.Lambda (name,s,t) as t' ->
-       (match l with
-           [] -> t'
-         | he::tl -> whdaux tl (S.subst he t)
-           (* when name is Anonimous the substitution should be superfluous *)
-       )
-    | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t)
-    | C.Appl (he::tl) -> whdaux (tl@l) he
-    | C.Appl [] -> raise (Impossible 1)
-    | C.Const (uri,exp_named_subst) as t ->
-	let o,_ = 
-	  CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
-	in
-       (match o with
-           C.Constant (_,Some body,_,_,_) ->
-            whdaux l (CicSubstitution.subst_vars exp_named_subst body)
-         | C.Constant _ -> if l = [] then t else C.Appl (t::l)
-         | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_,_,_) ->
-            whdaux l (CicSubstitution.subst_vars exp_named_subst body)
-         | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-       )
-    | C.MutInd _ as t -> if l = [] then t else C.Appl (t::l)
-    | C.MutConstruct _ as t -> if l = [] then t else C.Appl (t::l)
-    | C.MutCase (mutind,i,_,term,pl) as t->
-       let decofix =
-        function
-           C.CoFix (i,fl) as t ->
-            let (_,_,body) = List.nth fl i in
-             let body' =
-              let counter = ref (List.length fl) in
-               List.fold_right
-                (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                fl
-                body
-             in
-              whdaux [] body'
-         | C.Appl (C.CoFix (i,fl) :: tl) ->
-            let (_,_,body) = List.nth fl i in
-             let body' =
-              let counter = ref (List.length fl) in
-               List.fold_right
-                (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                fl
-                body
-             in
-              whdaux tl body'
-         | t -> t
-       in
-        (match decofix (whdaux [] term) with
-            C.MutConstruct (_,_,j,_) -> whdaux l (List.nth pl (j-1))
-          | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
-             let (arity, r) =
-	       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
-              match o with
-                 C.InductiveDefinition (tl,ingredients,r,_) ->
-                   let (_,_,arity,_) = List.nth tl i in
-                    (arity,r)
-               | _ -> raise WrongUriToInductiveDefinition
-             in
-              let ts =
-               let rec eat_first =
-                function
-                   (0,l) -> l
-                 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
-                 | _ -> raise (Impossible 5)
-               in
-                eat_first (r,tl)
-              in
-               whdaux (ts@l) (List.nth pl (j-1))
-          | C.Cast _ | C.Implicit _ ->
-             raise (Impossible 2) (* we don't trust our whd ;-) *)
-          | _ -> if l = [] then t else C.Appl (t::l)
-       )
-    | C.Fix (i,fl) as t ->
-       let (_,recindex,_,body) = List.nth fl i in
-        let recparam =
-         try
-          Some (List.nth l recindex)
-         with
-          _ -> None
-        in
-         (match recparam with
-             Some recparam ->
-              (match whdaux [] recparam with
-                  C.MutConstruct _
-                | C.Appl ((C.MutConstruct _)::_) ->
-                   let body' =
-                    let counter = ref (List.length fl) in
-                     List.fold_right
-                      (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
-                      fl
-                      body
-                   in
-                    (* Possible optimization: substituting whd recparam in l *)
-                    whdaux l body'
-               | _ -> if l = [] then t else C.Appl (t::l)
-             )
-          | None -> if l = [] then t else C.Appl (t::l)
-         )
-    | C.CoFix (i,fl) as t ->
-       if l = [] then t else C.Appl (t::l)
- in
-(*CSC
-function t ->
-prerr_endline ("PRIMA WHD" ^ CicPp.ppterm t) ; flush stderr ;
-List.iter (function (Cic.Decl t) -> prerr_endline ("Context: " ^ CicPp.ppterm t) | (Cic.Def t) -> prerr_endline ("Context:= " ^ CicPp.ppterm t)) context ; flush stderr ; prerr_endline "<PRIMA WHD" ; flush stderr ;
-let res =
-*)
-  whdaux []
-(*CSC
-t in prerr_endline "DOPO WHD" ; flush stderr ; res
-*)
-;;
-
-(* t1, t2 must be well-typed *)
-let are_convertible c t1 t2 ugraph =
- let module U = UriManager in
- let rec aux test_equality_only context t1 t2 ugraph =
-  let aux2 test_equality_only t1 t2 ugraph =
-   (* this trivial euristic cuts down the total time of about five times ;-) *)
-   (* this because most of the time t1 and t2 are "sintactically" the same   *)
-   if t1 = t2 then
-    true,ugraph
-   else
-    begin
-     let module C = Cic in
-       match (t1,t2) with
-          (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
-        | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
-            let b = U.eq uri1 uri2 in
-	    if b then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-                  (* FIXME: lazy! *)
-                  let b',ugraph' = aux test_equality_only context x y ugraph in
-                  (U.eq uri1 uri2 && b' && b),ugraph'
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph) 
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-	    else
-	      false,ugraph
-        | (C.Meta (n1,l1), C.Meta (n2,l2)) -> 
-            let b = n1 = n2 in
-	    if b then
-             List.fold_left2
-              (fun (b,ugraph) t1 t2 ->
-		if b then 
-                  match t1,t2 with
-                    None,_
-                  | _,None  -> true,ugraph
-                  | Some t1',Some t2' -> 
-		      aux test_equality_only context t1' t2' ugraph
-		else
-		  false,ugraph
-              ) (true,ugraph) l1 l2
-	    else
-	      false,ugraph
-          (* TASSI: CONSTRAINTS *)
-	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
-	    true,(CicUniv.add_eq t2 t1 ugraph)
-	  (* TASSI: CONSTRAINTS *)
-	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
-	    true,(CicUniv.add_ge t2 t1 ugraph)
-	  (* TASSI: CONSTRAINTS *)
-	| (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
-	  (* TASSI: CONSTRAINTS *)
-        | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
-        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-	    let b',ugraph' = aux true context s1 s2 ugraph in
-	    if b' then 
-              aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
-		t1 t2 ugraph'
-	    else
-	      false,ugraph
-        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
-           if b' then
-	     aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
-	       t1 t2 ugraph'
-	   else
-	     false,ugraph
-        | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
-           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
-	   if b' then
-            aux test_equality_only
-             ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
-	   else
-	     false,ugraph
-        | (C.Appl l1, C.Appl l2) ->
-           (try
-             List.fold_right2
-               (fun  x y (b,ugraph) -> 
-		 if b then
-		   aux test_equality_only context x y ugraph
-	         else
-	           false,ugraph) l1 l2 (true,ugraph)
-            with
-             Invalid_argument _ -> false,ugraph
-           )
-        | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
-            let b' = U.eq uri1 uri2 in
-	    if b' then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-		  if b && U.eq uri1 uri2 then
-		    aux test_equality_only context x y ugraph 
-		  else
-		    false,ugraph
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-	    else
-	      false,ugraph
-        | (C.MutInd (uri1,i1,exp_named_subst1),
-           C.MutInd (uri2,i2,exp_named_subst2)
-          ) ->
-            let b' = U.eq uri1 uri2 && i1 = i2 in
-	    if b' then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-                  if b && U.eq uri1 uri2 then
-		    aux test_equality_only context x y ugraph
-		  else
-		   false,ugraph
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-	    else 
-	      false,ugraph
-        | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
-           C.MutConstruct (uri2,i2,j2,exp_named_subst2)
-          ) ->
-            let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
-	    if b' then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-		  if b && U.eq uri1 uri2 then
-		    aux test_equality_only context x y ugraph
-		  else
-		    false,ugraph
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-	    else
-	      false,ugraph
-        | (C.MutCase (uri1,i1,outtype1,term1,pl1),
-           C.MutCase (uri2,i2,outtype2,term2,pl2)) -> 
-            let b' = U.eq uri1 uri2 && i1 = i2 in
-	    if b' then
-             let b'',ugraph''=aux test_equality_only context 
-		 outtype1 outtype2 ugraph in
-	     if b'' then 
-	       let b''',ugraph'''= aux test_equality_only context 
-		   term1 term2 ugraph'' in
-	       List.fold_right2
-		 (fun x y (b,ugraph) -> 
-		   if b then
-		     aux test_equality_only context x y ugraph 
-		   else 
-		     false,ugraph)
-		 pl1 pl2 (true,ugraph''')
-	     else
-	       false,ugraph
-	    else
-	      false,ugraph
-        | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-           let tys =
-            List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
-           in
-            if i1 = i2 then
-             List.fold_right2
-              (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
-                if b && recindex1 = recindex2 then
-		  let b',ugraph' = aux test_equality_only context ty1 ty2 
-		      ugraph in
-		  if b' then
-		    aux test_equality_only (tys@context) bo1 bo2 ugraph'
-	          else
-	            false,ugraph
-	        else
-	          false,ugraph)
-	     fl1 fl2 (true,ugraph)
-	    else
-	      false,ugraph
-        | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-           let tys =
-            List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
-           in
-            if i1 = i2 then
-              List.fold_right2
-              (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
-		if b then
-		  let b',ugraph' = aux test_equality_only context ty1 ty2 
-		      ugraph in
-		  if b' then
-		    aux test_equality_only (tys@context) bo1 bo2 ugraph'
-	          else
-	            false,ugraph
-	        else
-	          false,ugraph)
-	     fl1 fl2 (true,ugraph)
-	    else
-	      false,ugraph
-        | (C.Cast _, _) | (_, C.Cast _)
-        | (C.Implicit _, _) | (_, C.Implicit _) ->
-            assert false
-        | (_,_) -> false,ugraph
-    end
-  in
-   let b,ugraph' = aux2 test_equality_only t1 t2 ugraph in
-   if b then
-     b,ugraph'
-   else
-    begin
-     debug t1 [t2] "PREWHD";
-     let t1' = whd context t1 in
-     let t2' = whd context t2 in
-      debug t1' [t2'] "POSTWHD";
-      aux2 test_equality_only t1' t2' ugraph
-    end
- in
-  aux false c t1 t2 ugraph
-;;
diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.mli b/helm/ocaml/cic_proof_checking/cicReductionNaif.mli
deleted file mode 100644
index 624eebf5d..000000000
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.mli
+++ /dev/null
@@ -1,35 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-exception WrongUriToInductiveDefinition
-exception ReferenceToConstant
-exception ReferenceToVariable
-exception ReferenceToCurrentProof
-exception ReferenceToInductiveDefinition
-val fdebug : int ref
-val whd : Cic.context -> Cic.term -> Cic.term
-val are_convertible :
-	Cic.context -> Cic.term -> Cic.term -> 
-	CicUniv.universe_graph -> bool * CicUniv.universe_graph
diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index cd9773160..30a24c13a 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -417,10 +417,10 @@ if List.mem uri params then prerr_endline "---- OK2" ;
   substaux 1
 ;;
 
-(* lift_meta [t_1 ; ... ; t_n] t                                *)
+(* subst_meta [t_1 ; ... ; t_n] t                                *)
 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
 (* [t_i] is lifted as usual when it crosses an abstraction      *)
-let lift_meta l t = 
+let subst_meta l t = 
  let module C = Cic in
   if l = [] then t else 
    let rec aux k = function
diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index 1f0705881..b1c09277b 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
@@ -52,10 +52,8 @@ val subst : Cic.term -> Cic.term -> Cic.term
 val subst_vars :
  Cic.term Cic.explicit_named_substitution -> Cic.term -> Cic.term
 
-(* TODO CSC rename to subst_meta *)
-
-(* lift_meta [t_1 ; ... ; t_n] t                                *)
+(* subst_meta [t_1 ; ... ; t_n] t                                *)
 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
 (* [t_i] is lifted as usual when it crosses an abstraction      *)
-val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term
+val subst_meta : (Cic.term option) list -> Cic.term -> Cic.term
 
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2a7f8c4ae..fe46e4748 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1395,12 +1395,12 @@ and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
      function
          [] -> []
        | (Some (n,C.Decl t))::tl ->
-           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+           (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
        | (Some (n,C.Def (t,None)))::tl ->
-           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
        | None::tl -> None::(aux (i+1) tl)
        | (Some (n,C.Def (t,Some ty)))::tl ->
-           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
+           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
     in
      aux 1 canonical_context
    in
@@ -1482,15 +1482,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	      ~subst metasenv context canonical_context l ugraph
 	  in
             (* assuming subst is well typed !!!!! *)
-            ((CicSubstitution.lift_meta l ty), ugraph1)
-              (* type_of_aux context (CicSubstitution.lift_meta l term) *)
+            ((CicSubstitution.subst_meta l ty), ugraph1)
+              (* type_of_aux context (CicSubstitution.subst_meta l term) *)
 	with CicUtil.Subst_not_found _ ->
 	  let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
           let ugraph1 = 
 	    check_metasenv_consistency ~logger
 	      ~subst metasenv context canonical_context l ugraph
 	  in
-            ((CicSubstitution.lift_meta l ty),ugraph1))
+            ((CicSubstitution.subst_meta l ty),ugraph1))
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index eae88a14d..809c57dfe 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -33,52 +33,52 @@ type 'term pattern = [ `Goal | `Everywhere ]
   (* when an 'ident option is None, the default is to apply the tactic
   to the current goal *)
 
-type ('term, 'ident) tactic =
-  | LocatedTactic of CicAst.location * ('term, 'ident) tactic
+type loc = CicAst.location
 
-  | Absurd of 'term
-  | Apply of 'term
-  | Auto
-  | Assumption
-  | Change of 'term * 'term * 'ident option (* what, with what, where *)
-  | Change_pattern of 'term pattern * 'term * 'ident option
+type ('term, 'ident) tactic =
+  | Absurd of loc * 'term
+  | Apply of loc * 'term
+  | Auto of loc
+  | Assumption of loc
+  | Change of loc * 'term * 'term * 'ident option (* what, with what, where *)
+  | Change_pattern of loc * 'term pattern * 'term * 'ident option
       (* what, with what, where *)
-  | Contradiction
-  | Cut of 'term
-  | Decompose of 'ident * 'ident list (* where, which principles *)
-  | Discriminate of 'ident
-  | Elim of 'term * 'term option (* what to elim, which principle to use *)
-  | ElimType of 'term
-  | Exact of 'term
-  | Exists
-  | Fold of reduction_kind * 'term
-  | Fourier
-  | Hint
-  | Injection of 'ident
-  | Intros of int option * 'ident list
-  | Left
-  | LetIn of 'term * 'ident
-(*   | Named_intros of 'ident list (* joined with Intros above *) *)
-(*   | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) *)
-  | Reduce of reduction_kind * ('term list * 'term pattern) option
+  | Contradiction of loc
+  | Cut of loc * 'term
+  | Decompose of loc * 'ident * 'ident list (* where, which principles *)
+  | Discriminate of loc * 'ident
+  | Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
+  | ElimType of loc * 'term
+  | Exact of loc * 'term
+  | Exists of loc
+  | Fold of loc * reduction_kind * 'term
+  | Fourier of loc
+  | Goal of loc * int (* change current goal, argument is goal number 1-based *)
+  | Hint of loc
+  | Injection of loc * 'ident
+  | Intros of loc * int option * 'ident list
+  | Left of loc
+  | LetIn of loc * 'term * 'ident
+(*   | Named_intros of loc * 'ident list (* joined with Intros above *) *)
+(*   | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *)
+  | Reduce of loc * reduction_kind * ('term list * 'term pattern) option
       (* kind, (what, where)
       * if second argument is None, reduction is applied to the current goal,
-      * otherwise to each occurrence of terms given in list occuring in term
+      * otherwise to each occurrence of loc * terms given in list occuring in term
       * pattern *)
-  | Reflexivity
-  | Replace of 'term * 'term (* what, with what *)
-  | Replace_pattern of 'term pattern * 'term
-  | Rewrite of direction * 'term * 'ident option
-  | Right
-  | Ring
-  | Split
-  | Symmetry
-  | Transitivity of 'term
+  | Reflexivity of loc
+  | Replace of loc * 'term * 'term (* what, with what *)
+  | Replace_pattern of loc * 'term pattern * 'term
+  | Rewrite of loc * direction * 'term * 'ident option
+  | Right of loc
+  | Ring of loc
+  | Split of loc
+  | Symmetry of loc
+  | Transitivity of loc * 'term
 
 type thm_flavour =
   [ `Definition
   | `Fact
-  | `Goal
   | `Lemma
   | `Remark
   | `Theorem
@@ -92,46 +92,57 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 
 type print_kind = [ `Env | `Coer ]
 
+type 'term macro = 
+  | Abort of loc
+  | Print of loc * string
+  | Check of loc * 'term 
+  | Quit of loc
+  | Redo of loc * int option
+  | Undo of loc * int option
+(*   | Print of loc * print_kind *)
+  | Search_pat of loc * search_kind * string  (* searches with string pattern *)
+  | Search_term of loc * search_kind * 'term  (* searches with term pattern *)
+
+type alias_spec =
+  | Ident_alias of string * string        (* identifier, uri *)
+  | Symbol_alias of string * int * string (* name, instance no, description *)
+  | Number_alias of int * string          (* instance no, description *)
+
 type 'term command =
-  | Abort
-  | Baseuri of string option (** get/set base uri *)
-  | Basedir of string option (** get/set base dir *)
-  | Check of 'term 
-  | Search_pat of search_kind * string  (* searches with string pattern *)
-  | Search_term of search_kind * 'term  (* searches with term pattern *)
-  | Proof
-  | Qed of string option
+  | Set of loc * string * string
+  | Qed of loc
       (** name.
        * Name is needed when theorem was started without providing a name
        *)
-  | Quit
-  | Inductive of (string * 'term) list * 'term inductive_type list
-      (** parameters, list of mutual inductive types *)
-  | Theorem of thm_flavour * string option * 'term * 'term option
+  | Inductive of loc * (string * 'term) list * 'term inductive_type list
+      (** parameters, list of loc * mutual inductive types *)
+  | Theorem of loc * thm_flavour * string option * 'term * 'term option
       (** flavour, name, type, body
        * - name is absent when an unnamed theorem is being proved, tipically in
        *   interactive usage
        * - body is present when its given along with the command, otherwise it
        *   will be given in proof editing mode using the tactical language
        *)
-  | Coercion of 'term
-  | Redo of int option
-  | Undo of int option
-  | Print of print_kind
+  | Coercion of loc * 'term
+  | Alias of loc * alias_spec
 
 type ('term, 'ident) tactical =
-  | LocatedTactical of CicAst.location * ('term, 'ident) tactical
-
-  | Tactic of ('term, 'ident) tactic
-  | Command of 'term command
+  | Tactic of loc * ('term, 'ident) tactic
+  | Fail of loc
+  | Do of loc * int * ('term, 'ident) tactical
+  | IdTac of loc
+  | Repeat of loc * ('term, 'ident) tactical
+  | Seq of loc * ('term, 'ident) tactical list (* sequential composition *)
+  | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list
+  | Tries of loc * ('term, 'ident) tactical list
+      (* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
+  | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
 
-  | Fail
-  | Do of int * ('term, 'ident) tactical
-  | IdTac
-  | Repeat of ('term, 'ident) tactical
-  | Seq of ('term, 'ident) tactical list (* sequential composition *)
-  | Then of ('term, 'ident) tactical * ('term, 'ident) tactical list
-  | Tries of ('term, 'ident) tactical list
-      (* try a sequence of tacticals until one succeeds, fail otherwise *)
-  | Try of ('term, 'ident) tactical (* try a tactical and mask failures *)
+type ('term, 'ident) statement =
+  | Command of loc * 'term command
+  | Macro of loc * 'term macro 
+      (* Macro are substantially queries, but since we are not the kind of
+       * peolpe that like to push "start" to turn off the computer 
+       * we added this command *)
+  | Tactical of loc * ('term, 'ident) tactical
 
diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 80e3effce..74a6a749e 100644
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -39,57 +39,57 @@ open TacticAst
 let rec count_tactic current_size tac =
   if current_size > maxsize then current_size 
   else match tac with 
-      LocatedTactic (_, tac) -> count_tactic current_size tac
-    | Absurd term -> countterm (current_size + 6) term
-    | Apply term -> countterm (current_size + 6) term
-    | Auto -> current_size + 4
-    | Assumption -> current_size + 10
-    | Change (t1, t2, where) ->
+    | Absurd (_, term) -> countterm (current_size + 6) term
+    | Apply (_, term) -> countterm (current_size + 6) term
+    | Auto _ -> current_size + 4
+    | Assumption _ -> current_size + 10
+    | Change (_, t1, t2, where) ->
 	let size1 = countterm (current_size + 12) t1 in (* change, with *)
 	let size2 = countterm size1 t2 in
         (match where with 
 	     None -> size2
 	   | Some ident -> size2 + 3 + String.length ident)
-    | Change_pattern (_, _, _) -> assert false  (* TODO *)
-    | Contradiction -> current_size + 13
-    | Cut term -> countterm (current_size + 4) term
-    | Decompose (ident, principles) ->
+    | Change_pattern _ -> assert false  (* TODO *)
+    | Contradiction _ -> current_size + 13
+    | Cut (_, term) -> countterm (current_size + 4) term
+    | Decompose (_, ident, principles) ->
 	List.fold_left
 	  (fun size s -> size + (String.length s))
 	  (current_size + 11 + String.length ident) principles
-    | Discriminate ident -> current_size + 12 + (String.length ident)
-    | Elim (term, using) ->
+    | Discriminate (_, ident) -> current_size + 12 + (String.length ident)
+    | Elim (_, term, using) ->
 	let size1 = countterm (current_size + 5) term in
 	  (match using with 
 	   None -> size1
 	     | Some term -> countterm (size1 + 7) term)
-    | ElimType term -> countterm (current_size + 10) term
-    | Exact term -> countterm (current_size + 6) term
-    | Exists -> current_size + 6
-    | Fold (kind, term) ->
+    | ElimType (_, term) -> countterm (current_size + 10) term
+    | Exact (_, term) -> countterm (current_size + 6) term
+    | Exists _ -> current_size + 6
+    | Fold (_, kind, term) ->
 	countterm (current_size + 5) term
-    | Fourier -> current_size + 7
-    | Hint -> current_size + 4
-    | Injection ident -> current_size + 10 + (String.length ident)
-    | Intros (num, idents) ->
+    | Fourier _ -> current_size + 7
+    | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
+    | Hint _ -> current_size + 4
+    | Injection (_, ident) -> current_size + 10 + (String.length ident)
+    | Intros (_, num, idents) ->
 	List.fold_left 
 	  (fun size s -> size + (String.length s))
 	  (current_size + 7) idents
-    | Left -> current_size + 4
-    | LetIn (term, ident) ->
+    | Left _ -> current_size + 4
+    | LetIn (_, term, ident) ->
 	countterm (current_size + 5 + String.length ident) term
-    | Reduce (_, _) -> assert false  (* TODO *)
-    | Reflexivity -> current_size + 11
-    | Replace (t1, t2) -> 
+    | Reduce _ -> assert false  (* TODO *)
+    | Reflexivity _ -> current_size + 11
+    | Replace (_, t1, t2) -> 
 	let size1 = countterm (current_size + 14) t1 in (* replace, with *)
 	  countterm size1 t2	
-    | Replace_pattern (_, _) -> assert false  (* TODO *)
-    | Rewrite (_, _, _) -> assert false (* TODO *)
-    | Right -> current_size + 5
-    | Ring -> current_size + 4
-    | Split -> current_size + 5
-    | Symmetry -> current_size + 8
-    | Transitivity term -> 
+    | Replace_pattern _ -> assert false  (* TODO *)
+    | Rewrite _ -> assert false (* TODO *)
+    | Right _ -> current_size + 5
+    | Ring _ -> current_size + 4
+    | Split _ -> current_size + 5
+    | Symmetry _ -> current_size + 8
+    | Transitivity (_, term) -> 
 	countterm (current_size + 13) term
 ;;
 
@@ -126,17 +126,15 @@ let rec tactic2box tac =
     small_tactic2box tac
 
 and big_tactic2box = function
-    LocatedTactic (loc, tac) -> 
-      big_tactic2box tac
-  | Absurd term ->
+  | Absurd (_, term) ->
       Box.V([],[Box.Text([],"absurd");
 		ast2astBox term])
-  | Apply term -> 
+  | Apply (_, term) -> 
       Box.V([],[Box.Text([],"apply");
 		ast2astBox term])
-  | Assumption -> Box.Text([],"assumption")
-  | Auto -> Box.Text([],"auto")
-  | Change (t1, t2, where) ->
+  | Assumption _ -> Box.Text([],"assumption")
+  | Auto _ -> Box.Text([],"auto")
+  | Change (_, t1, t2, where) ->
       let where =
 	(match where with 
 	     None -> []
@@ -151,12 +149,12 @@ and big_tactic2box = function
 	      (pretty_append 
 		 [Box.Text([],"with")]
 		 t2)@where)
-  | Change_pattern (_, _, _) -> assert false  (* TODO *)
-  | Contradiction -> Box.Text([],"contradiction")
-  | Cut term -> 
+  | Change_pattern _ -> assert false  (* TODO *)
+  | Contradiction _ -> Box.Text([],"contradiction")
+  | Cut (_, term) -> 
       Box.V([],[Box.Text([],"cut");
 		Box.indent(ast2astBox term)])
-  | Decompose (ident, principles) ->
+  | Decompose (_, ident, principles) ->
       let principles =
 	List.map (fun x -> Box.Text([],x)) principles in
       Box.V([],[Box.Text([],"decompose");
@@ -164,10 +162,10 @@ and big_tactic2box = function
 			  Box.V([],principles);
 			  Box.Text([],"]")]);
 		Box.Text([],ident)])
-  | Discriminate ident -> 
+  | Discriminate (_, ident) -> 
       Box.V([],[Box.Text([],"discriminate");
 		Box.Text([],ident)])
-  | Elim (term, using) ->
+  | Elim (_, term, using) ->
       let using =
 	(match using with 
 	     None -> []
@@ -179,24 +177,25 @@ and big_tactic2box = function
 	    (pretty_append
 	       [Box.Text([],"elim")]
 	       term)@using)
-  | ElimType term -> 
+  | ElimType (_, term) -> 
       Box.V([],[Box.Text([],"elim type");
 		Box.indent(ast2astBox term)])
-  | Exact term -> 
+  | Exact (_, term) -> 
       Box.V([],[Box.Text([],"exact");
 		Box.indent(ast2astBox term)])
-  | Exists -> Box.Text([],"exists")
-  | Fold (kind, term) ->
+  | Exists _ -> Box.Text([],"exists")
+  | Fold (_, kind, term) ->
       Box.V([],[Box.H([],[Box.Text([],"fold");
 			  Box.smallskip;
 			  Box.Text([],string_of_kind kind)]);
 		Box.indent(ast2astBox term)])
-  | Fourier -> Box.Text([],"fourier")
-  | Hint -> Box.Text([],"hint")
-  | Injection ident -> 
+  | Fourier _ -> Box.Text([],"fourier")
+  | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
+  | Hint _ -> Box.Text([],"hint")
+  | Injection (_, ident) -> 
       Box.V([],[Box.Text([],"transitivity");
 		Box.indent (Box.Text([],ident))])
-  | Intros (num, idents) ->
+  | Intros (_, num, idents) ->
       let num =
 	(match num with 
 	     None -> [] 
@@ -206,17 +205,17 @@ and big_tactic2box = function
       Box.V([],[Box.Text([],"decompose");
 		Box.H([],[Box.smallskip;
 			  Box.V([],idents)])])
-  | Left -> Box.Text([],"left")
-  | LetIn (term, ident) ->
+  | Left _ -> Box.Text([],"left")
+  | LetIn (_, term, ident) ->
       Box.V([],[Box.H([],[Box.Text([],"let");
 			  Box.smallskip;
 			  Box.Text([],ident);
 			  Box.smallskip;
 			  Box.Text([],"=")]);
 		Box.indent (ast2astBox term)])
-  | Reduce (_, _) -> assert false  (* TODO *)
-  | Reflexivity -> Box.Text([],"reflexivity")
-  | Replace (t1, t2) -> 
+  | Reduce _ -> assert false  (* TODO *)
+  | Reflexivity _ -> Box.Text([],"reflexivity")
+  | Replace (_, t1, t2) -> 
       Box.V([],
 	    (pretty_append 
 	       [Box.Text([],"replace")]
@@ -224,13 +223,13 @@ and big_tactic2box = function
 	    (pretty_append 
 	       [Box.Text([],"with")]
 	       t2))
-  | Replace_pattern (_, _) -> assert false  (* TODO *)
-  | Rewrite (_, _, _) -> assert false (* TODO *)
-  | Right -> Box.Text([],"right")
-  | Ring ->  Box.Text([],"ring")
-  | Split -> Box.Text([],"split")
-  | Symmetry -> Box.Text([],"symmetry")
-  | Transitivity term -> 
+  | Replace_pattern _ -> assert false  (* TODO *)
+  | Rewrite _ -> assert false (* TODO *)
+  | Right _ -> Box.Text([],"right")
+  | Ring _ ->  Box.Text([],"ring")
+  | Split _ -> Box.Text([],"split")
+  | Symmetry _ -> Box.Text([],"symmetry")
+  | Transitivity (_, term) -> 
       Box.V([],[Box.Text([],"transitivity");
 		Box.indent (ast2astBox term)])
 ;;
@@ -238,35 +237,35 @@ and big_tactic2box = function
 open TacticAst
 
 let rec tactical2box = function
-  | LocatedTactical (loc, tac) -> tactical2box tac
-
-  | Tactic tac -> tactic2box tac
+  | Tactic (_, tac) -> tactic2box tac
+(*
   | Command cmd -> (* TODO dummy implementation *)
       Box.Text([], TacticAstPp.pp_tactical (Command cmd))
+*)
 
-  | Fail -> Box.Text([],"fail")
-  | Do (count, tac) -> 
+  | Fail _ -> Box.Text([],"fail")
+  | Do (_, count, tac) -> 
       Box.V([],[Box.Text([],"do " ^ string_of_int count);
 		Box.indent (tactical2box tac)])
-  | IdTac -> Box.Text([],"id")
-  | Repeat tac -> 
+  | IdTac _ -> Box.Text([],"id")
+  | Repeat (_, tac) -> 
       Box.V([],[Box.Text([],"repeat");
 		Box.indent (tactical2box tac)])
-  | Seq tacs -> 
+  | Seq (_, tacs) -> 
       Box.V([],tacticals2box tacs)
-  | Then (tac, tacs) -> 
+  | Then (_, tac, tacs) -> 
       Box.V([],[tactical2box tac;
 		Box.H([],[Box.skip;
 			  Box.Text([],"[");
 			  Box.V([],tacticals2box tacs);
 			  Box.Text([],"]");])])
-  | Tries tacs -> 
+  | Tries (_, tacs) -> 
       Box.V([],[Box.Text([],"try");
 		Box.H([],[Box.skip;
 			  Box.Text([],"[");
 			  Box.V([],tacticals2box tacs);
 			  Box.Text([],"]");])])
-  | Try tac -> 
+  | Try (_, tac) -> 
       Box.V([],[Box.Text([],"try");
 		Box.indent (tactical2box tac)])
 
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 0d539ddbe..1a28fa578 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -28,9 +28,11 @@ open Printf
 open TacticAst
 
 let tactical_terminator = "."
+let tactic_terminator = tactical_terminator
 let tactical_separator = ";"
 
-let pp_term term = CicAstPp.pp_term term
+let pp_term_ast term = CicAstPp.pp_term term
+let pp_term_cic term = CicPp.ppterm term
 
 let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 
@@ -40,57 +42,58 @@ let pp_reduction_kind = function
   | `Whd -> "whd"
 
 let rec pp_tactic = function
-  | LocatedTactic (loc, tac) -> pp_tactic tac
-  | Absurd term -> "absurd" ^ pp_term term
-  | Apply term -> "apply " ^ pp_term term
-  | Auto -> "auto"
-  | Assumption -> "assumption"
-  | Change (t1, t2, where) ->
-      sprintf "change %s with %s%s" (pp_term t1) (pp_term t2)
+  | Absurd (_, term) -> "absurd" ^ pp_term_ast term
+  | Apply (_, term) -> "apply " ^ pp_term_ast term
+  | Auto _ -> "auto"
+  | Assumption _ -> "assumption"
+  | Change (_, t1, t2, where) ->
+      sprintf "change %s with %s%s" (pp_term_ast t1) (pp_term_ast t2)
         (match where with None -> "" | Some ident -> "in " ^ ident)
-  | Change_pattern (_, _, _) -> assert false  (* TODO *)
-  | Contradiction -> "contradiction"
-  | Cut term -> "cut " ^ pp_term term
-  | Decompose (ident, principles) ->
+  | Change_pattern (_, _, _, _) -> assert false  (* TODO *)
+  | Contradiction _ -> "contradiction"
+  | Cut (_, term) -> "cut " ^ pp_term_ast term
+  | Decompose (_, ident, principles) ->
       sprintf "decompose %s %s" (pp_idents principles) ident
-  | Discriminate ident -> "discriminate " ^ ident
-  | Elim (term, using) ->
-      sprintf "elim " ^ pp_term term ^
-      (match using with None -> "" | Some term -> " using " ^ pp_term term)
-  | ElimType term -> "elim type " ^ pp_term term
-  | Exact term -> "exact " ^ pp_term term
-  | Exists -> "exists"
-  | Fold (kind, term) ->
-      sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term)
-  | Fourier -> "fourier"
-  | Hint -> "hint"
-  | Injection ident -> "injection " ^ ident
-  | Intros (None, []) -> "intro"
-  | Intros (num, idents) ->
+  | Discriminate (_, ident) -> "discriminate " ^ ident
+  | Elim (_, term, using) ->
+      sprintf "elim " ^ pp_term_ast term ^
+      (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
+  | ElimType (_, term) -> "elim type " ^ pp_term_ast term
+  | Exact (_, term) -> "exact " ^ pp_term_ast term
+  | Exists _ -> "exists"
+  | Fold (_, kind, term) ->
+      sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term)
+  | Goal (_, n) -> "goal " ^ string_of_int n
+  | Fourier _ -> "fourier"
+  | Hint _ -> "hint"
+  | Injection (_, ident) -> "injection " ^ ident
+  | Intros (_, None, []) -> "intro"
+  | Intros (_, num, idents) ->
       sprintf "intros%s%s"
         (match num with None -> "" | Some num -> " " ^ string_of_int num)
         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
-  | Left -> "left"
-  | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident
-  | Reduce (kind, None)
-  | Reduce (kind, Some ([], `Goal)) -> pp_reduction_kind kind
-  | Reduce (kind, Some ([], `Everywhere)) ->
+  | Left _ -> "left"
+  | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident
+  | Reduce (_, kind, None)
+  | Reduce (_, kind, Some ([], `Goal)) -> pp_reduction_kind kind
+  | Reduce (_, kind, Some ([], `Everywhere)) ->
       sprintf "%s in hyp" (pp_reduction_kind kind)
-  | Reduce (kind, Some (terms, `Goal)) ->
+  | Reduce (_, kind, Some (terms, `Goal)) ->
       sprintf "%s %s" (pp_reduction_kind kind)
-        (String.concat ", " (List.map pp_term terms))
-  | Reduce (kind, Some (terms, `Everywhere)) ->
+        (String.concat ", " (List.map pp_term_ast terms))
+  | Reduce (_, kind, Some (terms, `Everywhere)) ->
       sprintf "%s in hyp %s" (pp_reduction_kind kind)
-        (String.concat ", " (List.map pp_term terms))
-  | Reflexivity -> "reflexivity"
-  | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2)
-  | Replace_pattern (_, _) -> assert false  (* TODO *)
-  | Rewrite (_, _, _) -> assert false (* TODO *)
-  | Right -> "right"
-  | Ring -> "ring"
-  | Split -> "split"
-  | Symmetry -> "symmetry"
-  | Transitivity term -> "transitivity " ^ pp_term term
+        (String.concat ", " (List.map pp_term_ast terms))
+  | Reflexivity _ -> "reflexivity"
+  | Replace (_, t1, t2) ->
+      sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2)
+  | Replace_pattern (_, _, _) -> assert false  (* TODO *)
+  | Rewrite (_, _, _, _) -> assert false (* TODO *)
+  | Right _ -> "right"
+  | Ring _ -> "ring"
+  | Split _ -> "split"
+  | Symmetry _ -> "symmetry"
+  | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
 
 let pp_flavour = function
   | `Definition -> "Definition"
@@ -106,38 +109,51 @@ let pp_search_kind = function
   | `Match -> "match"
   | `Elim -> "elim"
 
-let pp_command = function
-  | Abort -> "Abort"
-  | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri
-  | Baseuri None -> "Baseuri"
-  | Check term -> sprintf "Check %s" (pp_term term)
-  | Proof -> "Proof"
-  | Qed name ->
-      (match name with None -> "Qed" | Some name -> sprintf "Save %s" name)
-  | Quit -> "Quit"
-  | Redo None -> "Redo"
-  | Redo (Some n) -> sprintf "Redo %d" n
-  | Search_pat (kind, pat) ->
+let pp_macro pp_term = function 
+  | Abort _ -> "Abort"
+  | Check (_, term) -> sprintf "Check %s" (pp_term term)
+  | Redo (_, None) -> "Redo"
+  | Redo (_, Some n) -> sprintf "Redo %d" n
+  | Search_pat (_, kind, pat) ->
       sprintf "search %s \"%s\"" (pp_search_kind kind) pat
-  | Search_term (kind, term) ->
+  | Search_term (_, kind, term) ->
       sprintf "search %s %s" (pp_search_kind kind) (pp_term term)
-  | Inductive (params, types) ->
+  | Undo (_, None) -> "Undo"
+  | Undo (_, Some n) -> sprintf "Undo %d" n
+  | Print (_, name) -> sprintf "Print \"%s\"" name
+  | Quit _ -> "Quit"
+
+let pp_macro_ast = pp_macro pp_term_ast
+let pp_macro_cic = pp_macro pp_term_cic
+
+let pp_alias = function
+  | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
+  | Symbol_alias (symb, instance, desc) ->
+      sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
+        symb instance desc
+  | Number_alias (instance,desc) ->
+      sprintf "alias num (instance %d) = \"%s\"" instance desc
+  
+let pp_command = function
+  | Qed _ -> "Qed"
+  | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
+  | Inductive (_, params, types) ->
       let pp_params = function
         | [] -> ""
         | params ->
             " " ^
             String.concat " "
               (List.map
-                (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ))
+                (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ))
                 params)
       in
       let pp_constructors constructors =
         String.concat "\n"
-          (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ))
+          (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ))
             constructors)
       in
       let pp_type (name, _, typ, constructors) =
-        sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ)
+        sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ)
           (pp_constructors constructors)
       in
       (match types with
@@ -146,37 +162,36 @@ let pp_command = function
           let fst_typ_pp =
             sprintf "%sinductive %s%s: %s \\def\n%s"
               (if inductive then "" else "co") name (pp_params params)
-              (pp_term typ) (pp_constructors constructors)
+              (pp_term_ast typ) (pp_constructors constructors)
           in
           fst_typ_pp ^ String.concat "" (List.map pp_type tl))
-  | Theorem (flavour, name, typ, body) ->
+  | Theorem (_, flavour, name, typ, body) ->
       sprintf "%s %s: %s %s"
         (pp_flavour flavour)
         (match name with None -> "" | Some name -> name)
-        (pp_term typ)
+        (pp_term_ast typ)
         (match body with
         | None -> ""
-        | Some body -> "\\def " ^ pp_term body)
-  | Undo None -> "Undo"
-  | Undo (Some n) -> sprintf "Undo %d" n
+        | Some body -> "\\def " ^ pp_term_ast body)
+  | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!"
+  | Alias (_,s) -> pp_alias s
 
 let rec pp_tactical = function
-  | LocatedTactical (loc, tac) -> pp_tactical tac
-
-  | Tactic tac -> pp_tactic tac
-  | Command cmd -> pp_command cmd
-
-  | Fail -> "fail"
-  | Do (count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
-  | IdTac -> "id"
-  | Repeat tac -> "repeat " ^ pp_tactical tac
-  | Seq tacs -> pp_tacticals tacs
-  | Then (tac, tacs) -> sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
-  | Tries tacs -> sprintf "tries [%s]" (pp_tacticals tacs)
-  | Try tac -> "try " ^ pp_tactical tac
+  | Tactic (_, tac) -> pp_tactic tac
+
+  | Fail _ -> "fail"
+  | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
+  | IdTac _ -> "id"
+  | Repeat (_, tac) -> "repeat " ^ pp_tactical tac
+  | Seq (_, tacs) -> pp_tacticals tacs
+  | Then (_, tac, tacs) ->
+      sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
+  | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals tacs)
+  | Try (_, tac) -> "try " ^ pp_tactical tac
 
 and pp_tacticals tacs =
   String.concat (tactical_separator ^ " ") (List.map pp_tactical tacs)
 
 let pp_tactical tac = pp_tactical tac ^ tactical_terminator
+let pp_tactic tac = pp_tactic tac ^ tactic_terminator
 
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli
index 356b07e76..f9fe2b2b8 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.mli
+++ b/helm/ocaml/cic_transformations/tacticAstPp.mli
@@ -24,6 +24,10 @@
  *)
 
 val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string
-
+val pp_command: CicAst.term TacticAst.command -> string
+val pp_macro: ('a -> string) -> 'a TacticAst.macro -> string
+val pp_macro_ast: CicAst.term TacticAst.macro -> string
+val pp_macro_cic: Cic.term TacticAst.macro -> string
 val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string
+val pp_alias: TacticAst.alias_spec -> string
 
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index d18458e2b..b8784d717 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -83,7 +83,7 @@ let rec deref subst =
       Cic.Meta(n,l) as t -> 
 	(try 
 	   deref subst
-	     (CicSubstitution.lift_meta 
+	     (CicSubstitution.subst_meta 
 		l (third (CicUtil.lookup_subst n subst))) 
 	 with 
 	   CicUtil.Subst_not_found _ -> t)
@@ -183,7 +183,7 @@ let apply_subst_gen ~appl_fun subst term =
     | C.Meta (i, l) -> 
         (try
           let (_, t,_) = lookup_subst i subst in
-          um_aux (S.lift_meta l t)
+          um_aux (S.subst_meta l t)
         with CicUtil.Subst_not_found _ -> 
 	  (* unconstrained variable, i.e. free in subst*)
           let l' =
@@ -657,7 +657,7 @@ let delift n subst context metasenv l t =
      | C.Meta (i, l1) as t -> 
          (try
            let (_,t,_) = CicUtil.lookup_subst i subst in
-             deliftaux k (CicSubstitution.lift_meta l1 t)
+             deliftaux k (CicSubstitution.subst_meta l1 t)
          with CicUtil.Subst_not_found _ ->
            (* see the top level invariant *)
            if (i = n) then 
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 8401ad5ad..621834e33 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -224,17 +224,17 @@ and type_of_aux' metasenv context t ugraph =
 		   canonical_context l ugraph 
                in
 		 (* trust or check ??? *)
-		 C.Meta (n,l'),CicSubstitution.lift_meta l' ty, 
+		 C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv', ugraph1
 		   (* type_of_aux subst metasenv 
-		      context (CicSubstitution.lift_meta l term) *)
+		      context (CicSubstitution.subst_meta l term) *)
              with CicUtil.Subst_not_found _ ->
                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
                let l',subst',metasenv', ugraph1 =
 		 check_metasenv_consistency n subst metasenv context
 		   canonical_context l ugraph
                in
-		 C.Meta (n,l'),CicSubstitution.lift_meta l' ty, 
+		 C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
                    subst', metasenv',ugraph1)
 	| C.Sort (C.Type tno) -> 
             let tno' = CicUniv.fresh() in 
@@ -605,14 +605,14 @@ and type_of_aux' metasenv context t ugraph =
 	function
             [] -> []
 	  | (Some (n,C.Decl t))::tl ->
-              (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+              (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 	  | (Some (n,C.Def (t,None)))::tl ->
-              (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+              (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 	  | None::tl -> None::(aux (i+1) tl)
 	  | (Some (n,C.Def (t,Some ty)))::tl ->
               (Some (n,
-		     C.Def ((S.lift_meta l (S.lift i t)),
-			    Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+		     C.Def ((S.subst_meta l (S.lift i t)),
+			    Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
       in
 	aux 1 canonical_context 
     in
diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index e521c6570..130799ea4 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -65,7 +65,7 @@ let rec deref subst =
       Cic.Meta(n,l) as t -> 
 	(try 
 	   deref subst
-	     (CicSubstitution.lift_meta 
+	     (CicSubstitution.subst_meta 
 		l (snd (CicUtil.lookup_subst n subst))) 
 	 with 
 	   CicUtil.Subst_not_found _ -> t)
@@ -99,7 +99,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
         | C.Meta (i,l) as t->
            (try
              let (_, t') = CicMetaSubst.lookup_subst i subst in
-             aux metasenv subst n context (CicSubstitution.lift_meta l t')
+             aux metasenv subst n context (CicSubstitution.subst_meta l t')
                ugraph
             with CicMetaSubst.SubstNotFound _ ->
               let (subst, metasenv, context, local_context,ugraph1) =
@@ -417,7 +417,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
         begin
         try
           let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-          let lifted_oldt = S.lift_meta l oldt in
+          let lifted_oldt = S.subst_meta l oldt in
           let ty_lifted_oldt,ugraph1 =
             type_of_aux' metasenv subst context lifted_oldt ugraph
           in
@@ -436,7 +436,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str
             let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in
              fo_unif_subst 
               test_equality_only 
-               subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
+               subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
           with AssertFailure _ ->
             (* TODO huge hack!!!!
              * we keep on unifying/refining in the hope that the problem will be
@@ -471,7 +471,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
             (* Unifying the types may have already instantiated n. Let's check *)
             try
              let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-             let lifted_oldt = S.lift_meta l oldt in
+             let lifted_oldt = S.subst_meta l oldt in
               fo_unif_subst_ordered 
                test_equality_only subst context metasenv t lifted_oldt ugraph2
             with
@@ -495,7 +495,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 	      in
 		fo_unif_subst 
 		  test_equality_only 
-		  subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
+		  subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
             with 
 		UnificationFailure msg 
 	      | Uncertain msg ->
@@ -532,7 +532,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 	 (* Unifying the types may have already instantiated n. Let's check *)
 	 try
 	   let (_, oldt,_) = CicUtil.lookup_subst n subst in
-	   let lifted_oldt = S.lift_meta l oldt in
+	   let lifted_oldt = S.subst_meta l oldt in
 	     fo_unif_subst_ordered 
 	       test_equality_only subst context metasenv t lifted_oldt ugraph2
 	 with
@@ -634,7 +634,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
 	  *)
             (try 
 	       let (_,t,_) = CicUtil.lookup_subst i subst in
-	       let lifted = S.lift_meta l t in
+	       let lifted = S.subst_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
 	       fo_unif_subst 
 		 test_equality_only 
@@ -649,7 +649,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
          | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
             (try 
 	       let (_,t,_) = CicUtil.lookup_subst i subst in
-	       let lifted = S.lift_meta l t in
+	       let lifted = S.subst_meta l t in
                let reduced = beta_reduce (Cic.Appl (lifted::args)) in
 	       fo_unif_subst 
 		 test_equality_only 
diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index 712e8aae2..6aad3676d 100644
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -25,11 +25,13 @@
 
 open Printf;;
 
+type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
+
 (* the list of known coercions (MUST be transitively closed) *)
 let coercions = ref [
   (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",
    UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con",
-   UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ;
+   UriManager.uri_of_string "cic:/Coq/Reals/Raxioms/INR.con") ;
 
    (
      UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)",
diff --git a/helm/ocaml/cic_unification/coercGraph.mli b/helm/ocaml/cic_unification/coercGraph.mli
index 9cbff65b9..cb0e51ca6 100644
--- a/helm/ocaml/cic_unification/coercGraph.mli
+++ b/helm/ocaml/cic_unification/coercGraph.mli
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
+
 val look_for_coercion :
   UriManager.uri -> UriManager.uri -> Cic.term option
 
diff --git a/helm/ocaml/hbugs/Makefile b/helm/ocaml/hbugs/Makefile
index af2d287ae..542bd2e3a 100644
--- a/helm/ocaml/hbugs/Makefile
+++ b/helm/ocaml/hbugs/Makefile
@@ -14,7 +14,7 @@
 PACKAGE = hbugs
 REQUIRES =	\
 	pcre lablgtk2.glade	\
-	helm-thread helm-xml helm-pxp helm-tactics
+	helm-thread helm-xml helm-pxp helm-tactics helm-registry
 
 IMPLEMENTATION_FILES = 			\
 	hbugs_misc.ml			\
diff --git a/helm/ocaml/hbugs/broker.ml b/helm/ocaml/hbugs/broker.ml
index 2ff8b9834..b86c08b9b 100644
--- a/helm/ocaml/hbugs/broker.ml
+++ b/helm/ocaml/hbugs/broker.ml
@@ -31,7 +31,6 @@ open Printf;;
 
 let debug = true ;;
 let debug_print s = if debug then prerr_endline s ;;
-Http_common.debug := false;;
 
 let daemon_name = "H-Bugs Broker" ;;
 let default_port = 49081 ;;
diff --git a/helm/ocaml/hbugs/hbugs_common.ml b/helm/ocaml/hbugs/hbugs_common.ml
index 3b19ceec0..6e060de7a 100644
--- a/helm/ocaml/hbugs/hbugs_common.ml
+++ b/helm/ocaml/hbugs/hbugs_common.ml
@@ -30,17 +30,17 @@ open Hbugs_types;;
 open Printf;;
 
 let rec string_of_hint = function
-  | Use_ring_Luke -> "Use Ring, Luke!"
-  | Use_fourier_Luke -> "Use Fourier, Luke!"
-  | Use_reflexivity_Luke -> "Use reflexivity, Luke!"
-  | Use_symmetry_Luke -> "Use symmetry, Luke!"
-  | Use_assumption_Luke -> "Use assumption, Luke!"
-  | Use_contradiction_Luke -> "Use contradiction, Luke!"
-  | Use_exists_Luke -> "Use exists, Luke!"
-  | Use_split_Luke -> "Use split, Luke!"
-  | Use_left_Luke -> "Use left, Luke!"
-  | Use_right_Luke -> "Use right, Luke!"
-  | Use_apply_Luke term -> sprintf "Apply %s, Luke!" term
+  | Use_ring -> "Use Ring, Luke!"
+  | Use_fourier -> "Use Fourier, Luke!"
+  | Use_reflexivity -> "Use reflexivity, Luke!"
+  | Use_symmetry -> "Use symmetry, Luke!"
+  | Use_assumption -> "Use assumption, Luke!"
+  | Use_contradiction -> "Use contradiction, Luke!"
+  | Use_exists -> "Use exists, Luke!"
+  | Use_split -> "Use split, Luke!"
+  | Use_left -> "Use left, Luke!"
+  | Use_right -> "Use right, Luke!"
+  | Use_apply term -> sprintf "Apply %s, Luke!" term
   | Hints hints -> String.concat "; " (List.map string_of_hint hints)
 ;;
 
diff --git a/helm/ocaml/hbugs/hbugs_messages.ml b/helm/ocaml/hbugs/hbugs_messages.ml
index d792c3250..a6aa34b31 100644
--- a/helm/ocaml/hbugs/hbugs_messages.ml
+++ b/helm/ocaml/hbugs/hbugs_messages.ml
@@ -100,17 +100,17 @@ let parse_state (root: ('a node extension as 'a) node) =
 let parse_hint node =
  let rec parse_hint_node node =
    match node#node_type with
-   | T_element "ring" -> Use_ring_Luke
-   | T_element "fourier" -> Use_fourier_Luke
-   | T_element "reflexivity" -> Use_reflexivity_Luke
-   | T_element "symmetry" -> Use_symmetry_Luke
-   | T_element "assumption" -> Use_assumption_Luke
-   | T_element "contradiction" -> Use_contradiction_Luke
-   | T_element "exists" -> Use_exists_Luke
-   | T_element "split" -> Use_split_Luke
-   | T_element "left" -> Use_left_Luke
-   | T_element "right" -> Use_right_Luke
-   | T_element "apply" -> Use_apply_Luke node#data
+   | T_element "ring" -> Use_ring
+   | T_element "fourier" -> Use_fourier
+   | T_element "reflexivity" -> Use_reflexivity
+   | T_element "symmetry" -> Use_symmetry
+   | T_element "assumption" -> Use_assumption
+   | T_element "contradiction" -> Use_contradiction
+   | T_element "exists" -> Use_exists
+   | T_element "split" -> Use_split
+   | T_element "left" -> Use_left
+   | T_element "right" -> Use_right
+   | T_element "apply" -> Use_apply node#data
    | T_element "hints" ->
        Hints
         (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
@@ -243,17 +243,17 @@ let pp_state = function
   | None -> "<gTopLevelStatus />\n"
 
 let rec pp_hint = function
-  | Use_ring_Luke -> sprintf "<ring />"
-  | Use_fourier_Luke -> sprintf "<fourier />"
-  | Use_reflexivity_Luke -> sprintf "<reflexivity />"
-  | Use_symmetry_Luke -> sprintf "<symmetry />"
-  | Use_assumption_Luke -> sprintf "<assumption />"
-  | Use_contradiction_Luke -> sprintf "<contradiction />"
-  | Use_exists_Luke -> sprintf "<exists />"
-  | Use_split_Luke -> sprintf "<split />"
-  | Use_left_Luke -> sprintf "<left />"
-  | Use_right_Luke -> sprintf "<right />"
-  | Use_apply_Luke term -> sprintf "<apply>%s</apply>" term
+  | Use_ring -> sprintf "<ring />"
+  | Use_fourier -> sprintf "<fourier />"
+  | Use_reflexivity -> sprintf "<reflexivity />"
+  | Use_symmetry -> sprintf "<symmetry />"
+  | Use_assumption -> sprintf "<assumption />"
+  | Use_contradiction -> sprintf "<contradiction />"
+  | Use_exists -> sprintf "<exists />"
+  | Use_split -> sprintf "<split />"
+  | Use_left -> sprintf "<left />"
+  | Use_right -> sprintf "<right />"
+  | Use_apply term -> sprintf "<apply>%s</apply>" term
   | Hints hints ->
       sprintf "<hints>\n%s\n</hints>"
         (String.concat "\n" (List.map pp_hint hints))
diff --git a/helm/ocaml/hbugs/hbugs_types.mli b/helm/ocaml/hbugs/hbugs_types.mli
index ebfa17994..e3067f2e9 100644
--- a/helm/ocaml/hbugs/hbugs_types.mli
+++ b/helm/ocaml/hbugs/hbugs_types.mli
@@ -37,17 +37,17 @@ type state =  (* proof assitant's state: proof type, proof body, goal *)
 
 type hint =
     (* tactics usage related hints *)
-  | Use_ring_Luke
-  | Use_fourier_Luke
-  | Use_reflexivity_Luke
-  | Use_symmetry_Luke
-  | Use_assumption_Luke
-  | Use_contradiction_Luke
-  | Use_exists_Luke
-  | Use_split_Luke
-  | Use_left_Luke
-  | Use_right_Luke
-  | Use_apply_Luke of string        (* use apply tactic on embedded term *)
+  | Use_ring
+  | Use_fourier
+  | Use_reflexivity
+  | Use_symmetry
+  | Use_assumption
+  | Use_contradiction
+  | Use_exists
+  | Use_split
+  | Use_left
+  | Use_right
+  | Use_apply of string        (* use apply tactic on embedded term *)
     (* hints list *)
   | Hints of hint list
 
diff --git a/helm/ocaml/hbugs/search_pattern_apply_tutor.ml b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml
index 0c1e7d0ae..1f5dad1bc 100644
--- a/helm/ocaml/hbugs/search_pattern_apply_tutor.ml
+++ b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml
@@ -40,7 +40,7 @@ let slave mqi_handle (state, musing_id) =
       if uris = [] then
         Sorry
       else
-        Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris))
+        Eureka (Hints (List.map (fun uri -> Use_apply uri) uris))
     with Empty_must -> Sorry
   in
   let answer = Musing_completed (my_own_id, musing_id, hint) in
diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 5ea64913d..0479264d4 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -47,7 +47,6 @@ let id_tac =
  in 
   mk_tactic tac
 
-
   (**
     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
     if one fails pass to the next one and so on, eventually raises (failure "no
@@ -110,9 +109,11 @@ let then_ ~start ~continuation =
  in
   mk_tactic (then_ ~start ~continuation)
 
-(* Galla *)
-(* si suppone che tutte le tattiche sollevino solamente Fail? *)
-
+let rec seq ~tactics =
+  match tactics with
+  | [] -> assert false
+  | [tac] -> tac
+  | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl)
 
 (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
 
@@ -187,6 +188,7 @@ let try_tactic ~tactic =
   mk_tactic (try_tactic ~tactic)
 ;;
 
+let fail = mk_tactic (fun _ -> raise (Fail "fail tactical"))
 
 (* This tries tactics until one of them doesn't _solve_ the goal *)
 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
diff --git a/helm/ocaml/tactics/tacticals.mli b/helm/ocaml/tactics/tacticals.mli
index 79a486acb..d7cc27545 100644
--- a/helm/ocaml/tactics/tacticals.mli
+++ b/helm/ocaml/tactics/tacticals.mli
@@ -38,6 +38,8 @@ val then_:
  start: ProofEngineTypes.tactic ->
  continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
 
+ (** "folding" of then_ *)
+val seq: tactics: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
 
 val repeat_tactic: 
  tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
@@ -52,7 +54,7 @@ val try_tactic:
 val solve_tactics:
  tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
 
-
+val fail: ProofEngineTypes.tactic
 
 (*
 val prova_tac : ProofEngineTypes.tactic
diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml
index 152e07b27..31364aa44 100644
--- a/helm/ocaml/tactics/tactics.ml
+++ b/helm/ocaml/tactics/tactics.ml
@@ -43,6 +43,7 @@ let exists = IntroductionTactics.exists_tac
 let fold = ReductionTactics.fold_tac
 let fourier = FourierR.fourier_tac
 let generalize = VariousTactics.generalize_tac
+let set_goal = VariousTactics.set_goal
 let injection = DiscriminationTactics.injection_tac
 let intros = PrimitiveTactics.intros_tac
 let left = IntroductionTactics.left_tac
diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 7b771249e..d70c94ac5 100644
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -32,6 +32,7 @@ val fourier : ProofEngineTypes.tactic
 val generalize :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   Cic.term list -> ProofEngineTypes.tactic
+val set_goal : int -> ProofEngineTypes.tactic
 val injection : term:Cic.term -> ProofEngineTypes.tactic
 val intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index be08c4d9e..c10060324 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -113,4 +113,12 @@ let generalize_tac
   PET.mk_tactic (generalize_tac mk_fresh_name_callback terms)
 ;;
 
+let set_goal n =
+  ProofEngineTypes.mk_tactic
+    (fun (proof, goal) ->
+       let (_, metasenv, _, _) = proof in
+       if CicUtil.exists_meta n metasenv then
+         (proof, [n])
+       else
+         raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n)))
 
diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli
index d1da2fe98..eefdd9846 100644
--- a/helm/ocaml/tactics/variousTactics.mli
+++ b/helm/ocaml/tactics/variousTactics.mli
@@ -27,8 +27,11 @@
 exception AllSelectedTermsMustBeConvertible;;
 
 val assumption_tac: ProofEngineTypes.tactic
+
 val generalize_tac:
  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list ->
   ProofEngineTypes.tactic
 
+  (* change the current goal to those referred by the given meta number *)
+val set_goal: int -> ProofEngineTypes.tactic
 
diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index 00cf4faa7..a4d260485 100644
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -36,6 +36,7 @@ let eq uri1 uri2 =
  uri1 == uri2
 ;;
 
+
 let string_of_uri uri =
   match  uri.(Array.length uri - 1) with
   | "" -> 
@@ -43,6 +44,8 @@ let string_of_uri uri =
   | _ -> 
       String.concat "#" 
         [ uri.(Array.length uri - 3); uri.(Array.length uri - 1) ]
+
+
 let name_of_uri uri = uri.(Array.length uri - 2);;
 let buri_of_uri uri = uri.(Array.length uri - 4);;
 let depth_of_uri uri = Array.length uri - 3;;
@@ -179,3 +182,16 @@ let string_of_uriref (uri, fi) =
       | [t]         -> str ^ xp t ^ ")" 
       | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" 
 
+let compare u1 u2 =
+  let su1 = string_of_uri u1 in
+  let su2 = string_of_uri u2 in
+  Pervasives.compare su1 su2
+
+module OrderedUri =
+struct
+  type t = uri
+  let compare = compare (* the one above, not Pervasives.compare *)
+end
+
+module UriSet = Set.Make (OrderedUri)
+
diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli
index 12775af8d..771def7c1 100644
--- a/helm/ocaml/urimanager/uriManager.mli
+++ b/helm/ocaml/urimanager/uriManager.mli
@@ -28,6 +28,7 @@ exception IllFormedUri of string;;
 type uri
 
 val eq : uri -> uri -> bool
+val compare : uri -> uri -> int
 
 val uri_of_string : string -> uri
 
@@ -67,3 +68,5 @@ val mutconstruct:     uri -> uri * int * int
 type uriref = uri * (int list)
 val string_of_uriref : uriref -> string
 
+module UriSet: Set.S with type elt = uri
+