Experimental merging of two functional graphs.

temporary synatx: 
Mergeschemes (G1 a b c) with (G2 a d e) using G1G2.

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

6 files changed, 793 insertions, 323 deletions

diff --git a/.depend b/.depend
index 25db9cebe..663242e7e 100644
--- a/.depend
+++ b/.depend
@@ -501,14 +501,15 @@ contrib/subtac/subtac_errors.cmi: lib/util.cmi lib/pp.cmi
 contrib/subtac/subtac_interp_fixpoint.cmi: lib/util.cmi interp/topconstr.cmi \
     lib/pp.cmi kernel/names.cmi library/libnames.cmi 
 contrib/subtac/subtac.cmi: toplevel/vernacexpr.cmo lib/util.cmi 
+contrib/subtac/subtac_obligations.cmi: kernel/term.cmi kernel/names.cmi 
 contrib/subtac/subtac_pretyping.cmi: interp/topconstr.cmi kernel/term.cmi \
     kernel/sign.cmi pretyping/pretyping.cmi kernel/names.cmi \
     library/global.cmi pretyping/evd.cmi kernel/environ.cmi 
 contrib/subtac/subtac_utils.cmi: lib/util.cmi interp/topconstr.cmi \
-    kernel/term.cmi proofs/tacexpr.cmo kernel/sign.cmi pretyping/rawterm.cmi \
-    proofs/proof_type.cmi lib/pp.cmi kernel/names.cmi library/libnames.cmi \
-    pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \
-    library/decl_kinds.cmo interp/coqlib.cmi 
+    kernel/term.cmi proofs/tacmach.cmi proofs/tacexpr.cmo kernel/sign.cmi \
+    pretyping/rawterm.cmi proofs/proof_type.cmi lib/pp.cmi kernel/names.cmi \
+    library/libnames.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+    kernel/environ.cmi library/decl_kinds.cmo interp/coqlib.cmi 
 contrib/xml/doubleTypeInference.cmi: kernel/term.cmi kernel/names.cmi \
     pretyping/evd.cmi kernel/environ.cmi contrib/xml/acic.cmo 
 contrib/xml/xmlcommand.cmi: contrib/xml/xml.cmi kernel/term.cmi \
@@ -3031,11 +3032,12 @@ contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
     pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \
     parsing/pptactic.cmi parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi \
     library/nametab.cmi kernel/names.cmi library/nameops.cmi \
-    parsing/lexer.cmi contrib/funind/invfun.cmo \
+    contrib/funind/merge.cmo parsing/lexer.cmi contrib/funind/invfun.cmo \
     contrib/funind/indfun_common.cmi contrib/funind/indfun.cmo \
     library/global.cmi interp/genarg.cmi \
-    contrib/funind/functional_principles_types.cmi parsing/egrammar.cmi \
-    interp/coqlib.cmi toplevel/cerrors.cmi 
+    contrib/funind/functional_principles_types.cmi pretyping/evd.cmi \
+    parsing/egrammar.cmi interp/coqlib.cmi interp/constrintern.cmi \
+    toplevel/cerrors.cmi 
 contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \
     tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \
@@ -3043,11 +3045,12 @@ contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
     pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \
     parsing/pptactic.cmx parsing/ppconstr.cmx lib/pp.cmx parsing/pcoq.cmx \
     library/nametab.cmx kernel/names.cmx library/nameops.cmx \
-    parsing/lexer.cmx contrib/funind/invfun.cmx \
+    contrib/funind/merge.cmx parsing/lexer.cmx contrib/funind/invfun.cmx \
     contrib/funind/indfun_common.cmx contrib/funind/indfun.cmx \
     library/global.cmx interp/genarg.cmx \
-    contrib/funind/functional_principles_types.cmx parsing/egrammar.cmx \
-    interp/coqlib.cmx toplevel/cerrors.cmx 
+    contrib/funind/functional_principles_types.cmx pretyping/evd.cmx \
+    parsing/egrammar.cmx interp/coqlib.cmx interp/constrintern.cmx \
+    toplevel/cerrors.cmx 
 contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \
     tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \
@@ -3108,14 +3111,20 @@ contrib/funind/invfun.cmx: toplevel/vernacentries.cmx lib/util.cmx \
     kernel/entries.cmx kernel/declarations.cmx library/decl_kinds.cmx \
     interp/coqlib.cmx toplevel/command.cmx kernel/closure.cmx \
     toplevel/cerrors.cmx 
-contrib/funind/merge.cmo: lib/util.cmi kernel/term.cmi \
-    contrib/funind/tacinvutils.cmi tactics/tacinterp.cmi kernel/names.cmi \
+contrib/funind/merge.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
+    interp/topconstr.cmi kernel/term.cmi tactics/tacinterp.cmi \
+    contrib/funind/rawtermops.cmi pretyping/rawterm.cmi parsing/printer.cmi \
+    pretyping/pretyping.cmi lib/pp.cmi lib/options.cmi kernel/names.cmi \
     pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \
-    pretyping/evd.cmi kernel/environ.cmi kernel/declarations.cmi 
-contrib/funind/merge.cmx: lib/util.cmx kernel/term.cmx \
-    contrib/funind/tacinvutils.cmx tactics/tacinterp.cmx kernel/names.cmx \
+    pretyping/evd.cmi kernel/environ.cmi pretyping/detyping.cmi \
+    kernel/declarations.cmi interp/constrextern.cmi toplevel/command.cmi 
+contrib/funind/merge.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
+    interp/topconstr.cmx kernel/term.cmx tactics/tacinterp.cmx \
+    contrib/funind/rawtermops.cmx pretyping/rawterm.cmx parsing/printer.cmx \
+    pretyping/pretyping.cmx lib/pp.cmx lib/options.cmx kernel/names.cmx \
     pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \
-    pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx 
+    pretyping/evd.cmx kernel/environ.cmx pretyping/detyping.cmx \
+    kernel/declarations.cmx interp/constrextern.cmx toplevel/command.cmx 
 contrib/funind/rawtermops.cmo: lib/util.cmi pretyping/rawterm.cmi lib/pp.cmi \
     kernel/names.cmi library/nameops.cmi library/libnames.cmi \
     pretyping/inductiveops.cmi contrib/funind/indfun_common.cmi \
@@ -3661,7 +3670,7 @@ contrib/subtac/g_eterm.cmx: lib/util.cmx proofs/tacmach.cmx \
 contrib/subtac/g_subtac.cmo: toplevel/vernacinterp.cmi \
     toplevel/vernacexpr.cmo toplevel/vernacentries.cmi lib/util.cmi \
     interp/topconstr.cmi kernel/term.cmi proofs/tacexpr.cmo \
-    contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac.cmi \
+    contrib/subtac/subtac_obligations.cmi contrib/subtac/subtac.cmi \
     kernel/reduction.cmi proofs/proof_type.cmi lib/pp.cmi parsing/pcoq.cmi \
     lib/options.cmi kernel/names.cmi library/nameops.cmi library/libnames.cmi \
     interp/genarg.cmi parsing/egrammar.cmi toplevel/cerrors.cmi 
@@ -3677,26 +3686,28 @@ contrib/subtac/subtac_coercion.cmo: lib/util.cmi kernel/typeops.cmi \
     contrib/subtac/subtac_errors.cmi pretyping/retyping.cmi \
     pretyping/reductionops.cmi kernel/reduction.cmi pretyping/recordops.cmi \
     pretyping/rawterm.cmi parsing/printer.cmi pretyping/pretype_errors.cmi \
-    lib/pp.cmi kernel/names.cmi library/global.cmi pretyping/evd.cmi \
-    pretyping/evarutil.cmi pretyping/evarconv.cmi contrib/subtac/eterm.cmi \
-    kernel/environ.cmi interp/coqlib.cmi contrib/subtac/context.cmi \
-    pretyping/classops.cmi contrib/subtac/subtac_coercion.cmi 
+    lib/pp.cmi kernel/names.cmi library/nameops.cmi library/global.cmi \
+    pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \
+    contrib/subtac/eterm.cmi kernel/environ.cmi interp/coqlib.cmi \
+    contrib/subtac/context.cmi pretyping/classops.cmi \
+    contrib/subtac/subtac_coercion.cmi 
 contrib/subtac/subtac_coercion.cmx: lib/util.cmx kernel/typeops.cmx \
     pretyping/termops.cmx kernel/term.cmx contrib/subtac/subtac_utils.cmx \
     contrib/subtac/subtac_errors.cmx pretyping/retyping.cmx \
     pretyping/reductionops.cmx kernel/reduction.cmx pretyping/recordops.cmx \
     pretyping/rawterm.cmx parsing/printer.cmx pretyping/pretype_errors.cmx \
-    lib/pp.cmx kernel/names.cmx library/global.cmx pretyping/evd.cmx \
-    pretyping/evarutil.cmx pretyping/evarconv.cmx contrib/subtac/eterm.cmx \
-    kernel/environ.cmx interp/coqlib.cmx contrib/subtac/context.cmx \
-    pretyping/classops.cmx contrib/subtac/subtac_coercion.cmi 
+    lib/pp.cmx kernel/names.cmx library/nameops.cmx library/global.cmx \
+    pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \
+    contrib/subtac/eterm.cmx kernel/environ.cmx interp/coqlib.cmx \
+    contrib/subtac/context.cmx pretyping/classops.cmx \
+    contrib/subtac/subtac_coercion.cmi 
 contrib/subtac/subtac_command.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \
     kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
     proofs/tactic_debug.cmi pretyping/tacred.cmi proofs/tacmach.cmi \
     tactics/tacinterp.cmi proofs/tacexpr.cmo interp/syntax_def.cmi \
     contrib/subtac/subtac_utils.cmi contrib/subtac/subtac_pretyping.cmi \
-    contrib/subtac/subtac_obligations.cmo library/states.cmi kernel/sign.cmi \
+    contrib/subtac/subtac_obligations.cmi library/states.cmi kernel/sign.cmi \
     kernel/safe_typing.cmi interp/reserve.cmi proofs/refiner.cmi \
     pretyping/reductionops.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \
     parsing/printer.cmi pretyping/pretyping.cmi parsing/ppconstr.cmi \
@@ -3793,13 +3804,17 @@ contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
 contrib/subtac/subtac_obligations.cmo: lib/util.cmi kernel/term.cmi \
     library/summary.cmi contrib/subtac/subtac_utils.cmi lib/pp.cmi \
     lib/options.cmi kernel/names.cmi library/libobject.cmi \
-    library/libnames.cmi kernel/entries.cmi library/declare.cmi \
-    library/decl_kinds.cmo toplevel/command.cmi 
+    library/libnames.cmi pretyping/evd.cmi kernel/environ.cmi \
+    kernel/entries.cmi library/declare.cmi library/decl_kinds.cmo \
+    toplevel/command.cmi tactics/auto.cmi \
+    contrib/subtac/subtac_obligations.cmi 
 contrib/subtac/subtac_obligations.cmx: lib/util.cmx kernel/term.cmx \
     library/summary.cmx contrib/subtac/subtac_utils.cmx lib/pp.cmx \
     lib/options.cmx kernel/names.cmx library/libobject.cmx \
-    library/libnames.cmx kernel/entries.cmx library/declare.cmx \
-    library/decl_kinds.cmx toplevel/command.cmx 
+    library/libnames.cmx pretyping/evd.cmx kernel/environ.cmx \
+    kernel/entries.cmx library/declare.cmx library/decl_kinds.cmx \
+    toplevel/command.cmx tactics/auto.cmx \
+    contrib/subtac/subtac_obligations.cmi 
 contrib/subtac/subtac_pretyping_F.cmo: lib/util.cmi kernel/typeops.cmi \
     kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \
     kernel/sign.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \
@@ -3824,7 +3839,7 @@ contrib/subtac/subtac_pretyping.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     kernel/typeops.cmi kernel/type_errors.cmi interp/topconstr.cmi \
     pretyping/termops.cmi kernel/term.cmi contrib/subtac/subtac_utils.cmi \
     contrib/subtac/subtac_pretyping_F.cmo \
-    contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac_errors.cmi \
+    contrib/subtac/subtac_obligations.cmi contrib/subtac/subtac_errors.cmi \
     contrib/subtac/subtac_coercion.cmi kernel/sign.cmi \
     pretyping/reductionops.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \
     parsing/printer.cmi pretyping/pretype_errors.cmi lib/pp.cmi \
@@ -3850,21 +3865,23 @@ contrib/subtac/subtac_pretyping.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
     contrib/subtac/subtac_pretyping.cmi 
 contrib/subtac/subtac_utils.cmo: lib/util.cmi interp/topconstr.cmi \
     pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \
-    tactics/tacticals.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \
-    proofs/proof_type.cmi parsing/printer.cmi pretyping/pretype_errors.cmi \
-    parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi lib/options.cmi \
-    kernel/names.cmi library/libnames.cmi library/global.cmi \
-    pretyping/evd.cmi pretyping/evarutil.cmi library/decl_kinds.cmo \
-    interp/coqlib.cmi interp/constrextern.cmi toplevel/command.cmi \
+    tactics/tacticals.cmi proofs/tacmach.cmi proofs/tacexpr.cmo \
+    pretyping/rawterm.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \
+    parsing/printer.cmi pretyping/pretype_errors.cmi parsing/ppconstr.cmi \
+    lib/pp.cmi proofs/pfedit.cmi lib/options.cmi kernel/names.cmi \
+    library/libnames.cmi library/global.cmi pretyping/evd.cmi \
+    pretyping/evarutil.cmi library/decl_kinds.cmo interp/coqlib.cmi \
+    interp/constrextern.cmi toplevel/command.cmi \
     contrib/subtac/subtac_utils.cmi 
 contrib/subtac/subtac_utils.cmx: lib/util.cmx interp/topconstr.cmx \
     pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \
-    tactics/tacticals.cmx proofs/tacexpr.cmx pretyping/rawterm.cmx \
-    proofs/proof_type.cmx parsing/printer.cmx pretyping/pretype_errors.cmx \
-    parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx lib/options.cmx \
-    kernel/names.cmx library/libnames.cmx library/global.cmx \
-    pretyping/evd.cmx pretyping/evarutil.cmx library/decl_kinds.cmx \
-    interp/coqlib.cmx interp/constrextern.cmx toplevel/command.cmx \
+    tactics/tacticals.cmx proofs/tacmach.cmx proofs/tacexpr.cmx \
+    pretyping/rawterm.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \
+    parsing/printer.cmx pretyping/pretype_errors.cmx parsing/ppconstr.cmx \
+    lib/pp.cmx proofs/pfedit.cmx lib/options.cmx kernel/names.cmx \
+    library/libnames.cmx library/global.cmx pretyping/evd.cmx \
+    pretyping/evarutil.cmx library/decl_kinds.cmx interp/coqlib.cmx \
+    interp/constrextern.cmx toplevel/command.cmx \
     contrib/subtac/subtac_utils.cmi 
 contrib/xml/acic2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi kernel/term.cmi \
     kernel/names.cmi contrib/xml/cic2acic.cmo contrib/xml/acic.cmo 
@@ -4121,66 +4138,74 @@ tools/coq_makefile.cmx:
 tools/coq-tex.cmo: 
 tools/coq-tex.cmx: 
 coq_fix_code.o: kernel/byterun/coq_fix_code.c \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/mlvalues.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \
   kernel/byterun/coq_fix_code.h
 coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  kernel/byterun/coq_jumptbl.h
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \
+  kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h
 coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/fail.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  /usr/lib/ocaml/caml/alloc.h
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h
 coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/misc.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/mlvalues.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \
   kernel/byterun/coq_fix_code.h
 coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  kernel/byterun/coq_jumptbl.h
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \
+  kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/alloc.h /usr/lib/ocaml/caml/mlvalues.h \
-  kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
-  kernel/byterun/coq_memory.h /usr/lib/ocaml/caml/config.h \
-  /usr/lib/ocaml/caml/fail.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+  kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h
 coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/compatibility.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
+  /usr/lib/ocaml/3.09.2/caml/compatibility.h \
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/caml/config.h /usr/lib/ocaml/caml/fail.h \
-  /usr/lib/ocaml/caml/mlvalues.h /usr/lib/ocaml/caml/misc.h \
-  /usr/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
-  /usr/lib/ocaml/caml/alloc.h
+  /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
+  /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+  /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \
+  /usr/lib/ocaml/3.09.2/caml/alloc.h
diff --git a/Makefile b/Makefile
index 831f70333..55035e36a 100644
--- a/Makefile
+++ b/Makefile
@@ -288,7 +288,7 @@ FUNINDCMO=\
   contrib/funind/functional_principles_proofs.cmo \
   contrib/funind/functional_principles_types.cmo \
   contrib/funind/invfun.cmo contrib/funind/indfun.cmo \
-  contrib/funind/indfun_main.cmo
+  contrib/funind/merge.cmo contrib/funind/indfun_main.cmo
 
 RECDEFCMO=\
   contrib/recdef/recdef.cmo
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index d1b989fdb..26a1066c0 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -438,13 +438,12 @@ TACTIC EXTEND poseq
       [ poseq x c ]
 END
 
-(*
 VERNAC COMMAND EXTEND Showindinfo
   [ "showindinfo" ident(x) ] -> [ Merge.showind x ]
 END
 
 VERNAC COMMAND EXTEND MergeFunind
-  [ "Mergeschemes" lconstr(c) "with" lconstr(c')  ] -> 
+  [ "Mergeschemes" lconstr(c) "with" lconstr(c') "using" ident(id) ] -> 
      [ 
        let c1 = Constrintern.interp_constr Evd.empty (Global.env()) c in
        let c2 = Constrintern.interp_constr Evd.empty (Global.env()) c' in
@@ -463,7 +462,6 @@ VERNAC COMMAND EXTEND MergeFunind
 	 with Invalid_argument _ 
 	     -> Util.error ("Bad argument form for merging schemes") in
        (* TOFO: enlever le ignore et declarer l'inductif *)
-       ignore(Merge.merge c1 c2 args1 args2)
+       ignore(Merge.merge c1 c2 args1 args2 id)
      ]
 END
-*)
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 35fb141a6..295ac604a 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -10,17 +10,22 @@
 
 (*i $Id: i*)
 
-(*i*)
+open Util
+open Topconstr
+open Vernacexpr
+open Pp
 open Names
 open Term
 open Declarations
 open Environ
-(*i*)
+open Rawterm
+open Rawtermops
 
+(** {1 Utilities}  *)
 
+(** {2 Useful operations on constr and rawconstr} *)
 
-(* Substitutions in constr *)
-
+(** Substitutions in constr *)
 let compare_constr_nosub t1 t2 =
   if compare_constr (fun _ _ -> false) t1 t2 
   then true
@@ -37,68 +42,288 @@ let rec substitterm prof t by_t in_u =
   else map_constr_with_binders succ 
     (fun i -> substitterm i t by_t) prof in_u
 
-(* Parameters shifting information. *)
+let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl
+
+let understand = Pretyping.Default.understand Evd.empty (Global.env())
+
+(** Operations on names *)
+let id_of_name = function
+    Anonymous -> id_of_string "H"
+  | Name id   -> id;;
+let name_of_string str = Name (id_of_string str)
+let string_of_name nme = string_of_id (id_of_name nme)
+
+(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
+let isVarf f x = 
+    match x with
+      | RVar (_,x) -> x = f 
+      | _ -> false
+
+
+(** {2 Debugging} *)
+(* comment this line to see debug msgs *)
+let msg x = () ;; let pr_lconstr c = str ""
+(* uncomment this to see debugging *)
+let prconstr c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
+let prlistconstr lc = List.iter prconstr lc
+let prstr s = msg(str s)
+let prNamedConstr s c = 
+  begin
+    msg(str "");
+    msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n");
+    msg(str "");
+  end
+let prNamedRConstr s c = 
+  begin
+    msg(str "");
+    msg(str(s^"==>\n ") ++ Printer.pr_rawconstr c ++ str "\n<==\n");
+    msg(str "");
+  end
+let prNamedLConstr_aux lc = 
+  List.iter (prNamedConstr "#>") lc
+let prNamedLConstr s lc = 
+  begin
+    prstr s;
+    prNamedLConstr_aux lc
+  end
+let prNamedLDecl s lc = 
+  begin
+    prstr s; prstr "\n";
+    List.iter (fun (nm,_,tp) -> prNamedConstr (string_of_name nm) tp) lc;
+    prstr "\n";
+  end
+
+let showind (id:identifier) =
+  let cstrid = Tacinterp.constr_of_id (Global.env()) id in
+  let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
+  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
+  List.iter (fun (nm, optcstr, tp) -> 
+    print_string (string_of_name nm^":");
+    prconstr tp; print_string "\n") 
+    ib1.mind_arity_ctxt;
+  (match ib1.mind_arity with
+    | Monomorphic x ->
+        Printf.printf "arity :"; prconstr x.mind_user_arity
+    | Polymorphic x -> 
+        Printf.printf "arity : universe?");
+  Array.iteri 
+    (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
+    ib1.mind_user_lc
+
+(** {2 Misc} *)
+
+exception Found of int
+
+(* Array scanning *)
+let array_find (arr: 'a array) (pred: int -> 'a -> bool): int option = 
+  try
+    for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
+    None
+  with Found i -> Some i
+
+let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
+  try
+    for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
+    Array.length arr (* all elt are positive *)
+  with Found i -> i
+
+let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a = 
+  let i = ref 0 in 
+  Array.fold_left 
+    (fun acc x -> 
+      let res = f !i acc x in i := !i + 1; res)
+    acc arr
+
+(* Like list_chop but except that [i] is the size of the suffix of [l]. *)
+let list_chop_end i l =
+  let size_prefix = List.length l -i in
+  if size_prefix < 0 then failwith "list_chop_end"
+  else list_chop size_prefix l
+
+let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a = 
+  let i = ref 0 in 
+  List.fold_left 
+    (fun acc x -> 
+      let res = f !i acc x in i := !i + 1; res)
+    acc arr
+
+let list_filteri (f: int -> 'a -> bool) (l:'a list):'a list = 
+  let i = ref 0 in 
+  List.filter (fun x -> let res = f !i x in i := !i + 1; res) l
+
+
+(** Iteration module *)
+module For = 
+struct
+  let rec map i j (f: int -> 'a)  = if i>j then [] else f i :: (map (i+1) j f)
+  let rec foldup i j (f: 'a -> int -> 'a) acc = 
+    if i>j then acc else let newacc = f acc i in foldup (i+1) j f newacc
+  let rec folddown i j (f: 'a -> int -> 'a) acc = 
+    if i>j then acc else let newacc = f acc j in folddown i (j-1) f newacc
+  let fold i j = if i<j then foldup i j else folddown i j
+end
+
+
+(** {1 Parameters shifting and linking information} *)
+
+(** This type is used to deal with debruijn linked indices. When a
+    variable is linked to a previous one, we will ignore it and refer
+    to previous one. *)
+type linked_var =
+    | Linked of int
+    | Unlinked
+
+(** When merging two graphs, parameters may become regular arguments,
+    and thus be shifted. This type describe the result of computing
+    the changes. *)
 type 'a shifted_params =
     {
       nprm1:'a;
       nprm2:'a;
+      prm2_unlinked:'a list; (* ranks of unlinked params in nprms2 *)
       nuprm1:'a;
       nuprm2:'a;
+      nargs1:'a;
+      nargs2:'a;
     }
 
-(* This type is used to deal with debruijn linked indices. When a
-   variable is linke to a previous one, we will ignore it and refer to
-   previous one. *)
-type linked_var =
-    | Linked of int
-    | Unlinked of int
 
 let prlinked x =
   match x with
     | Linked i -> Printf.sprintf "Linked %d" i
-    | Unlinked i -> Printf.sprintf "Unlinked %d" i
+    | Unlinked -> Printf.sprintf "Unlinked"
 
 let linkmonad f lnkvar = 
   match lnkvar with
     | Linked i -> Linked (f i)
-    | Unlinked i -> Unlinked (f i)
+    | Unlinked -> Unlinked
 
 let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar
 
 (* This map is used to deal with debruijn linked indices. *)
 module Link = Map.Make (struct type t = int let compare = Pervasives.compare end)
-let poplink n l: 'a Link.t = 
-  Link.fold 
-    (fun k e acc -> Link.add (k-n) (linklift e (-k)) acc)
-    l Link.empty 
 
+let pr_links l = 
+  Printf.printf "links:\n";
+  Link.iter (fun k e -> Printf.printf "%d : %s\n" k (prlinked e)) l;
+  Printf.printf "_____________\n"
+
+type 'a merged_arg =
+    | Prm_stable of 'a
+    | Prm_linked of 'a
+    | Prm_arg of 'a
+    | Arg_stable of 'a
+    | Arg_linked of 'a
+
+type merge_infos =
+    {
+      ident:identifier; (* new inductive name *)
+      mib1: mutual_inductive_body;
+      oib1: one_inductive_body; 
+      mib2: mutual_inductive_body;
+      oib2: one_inductive_body; 
+      (* Array of links of the first inductive (should be all stable) *)
+      lnk1: int merged_arg array;
+      (* Array of links of the second inductive (point to the first ind param/args) *)
+      lnk2: int merged_arg array;
+      (* number of rec params of ind1 which remai rec param in merge *)
+      nrecprms1: int;
+      (* number of other rec params of ind1 (which become non parm) *)
+      notherprms1:int;
+      (* list of decl of rec parms from ind1 which remain parms *)
+      recprms1: rel_declaration list;
+      (* List of other rec parms from ind1 *)
+      otherprms1: rel_declaration list; (* parms that became args *)
+      (* number of rec params of ind2 which remain rec param in merge (and not linked) *)
+      nrecprms2: int;
+      (* number of other rec params of ind2 (which become non parm) *)
+      notherprms2:int;
+      (* list of decl of rec parms from ind2 which remain parms (and not linked) *)
+      recprms2: rel_declaration list;
+      (* List of other rec parms from ind2 (which are linked or become non parm) *)
+      otherprms2: rel_declaration list;      
+      (* list of decl of ordinary args from ind1 which remain args in merge *)
+(*      args1:rel_declaration list;
+      (* list of decl of ordinary args from ind2 which remain args in merge *)
+      args2:rel_declaration list;
+      nargs1:int;
+      nargs2:int*)
+    }
+
+
+let pr_merginfo x =
+  let i,s=
+    match x with 
+      | Prm_linked i -> i,"Prm_linked"
+      | Arg_linked i -> i,"Arg_linked"
+      | Prm_stable i ->  i,"Prm_stable"
+      | Prm_arg i ->  i,"Prm_arg"
+      | Arg_stable i ->  i,"Arg_stable" in
+  (Printf.sprintf "%s(%d)" s i)
+
+let mrgarg_linked x =
+  match x with Prm_linked _ | Arg_linked _ -> true | _ -> false
+
+let mrgarg_wasparm x =
+  match x with Prm_stable _ | Prm_linked _ | Prm_arg _ -> true | _ -> false
+
+let mrgarg_wasarg x =
+  match x with Arg_stable _ | Arg_linked _ -> true | _ -> false
+  
+let mrgarg_stblparm x = match x with Prm_stable _ -> true | _ -> false
 
-let liftlink n l: 'a Link.t =
-   Link.fold 
-    (fun k e acc -> Link.add (k+n) (linklift e k) acc)
-    l Link.empty 
+let mrgarg_stblarg x = match x with Arg_stable _ -> true | _ -> false
 
+let filter_shift (lnk:int merged_arg array) (l:'a list): 'a list =
+  let prms = list_filteri (fun i _ -> mrgarg_stblparm lnk.(i)) l in
+  let args = list_filteri (fun i _ -> mrgarg_stblarg lnk.(i)) l in
+  prms@args
 
-(* Reverse the link map, keeping only linked vars, elements are list
-   of int as several vars may be linked to the same var. *)
+(** Reverse the link map, keeping only linked vars, elements are list
+    of int as several vars may be linked to the same var. *)
 let revlinked lnk =
-  Link.fold 
-    (fun k x acc -> 
-      match x with 
-        | Unlinked _ -> acc 
+  For.fold 0 (Array.length lnk - 1)
+    (fun acc k -> 
+      match lnk.(k) with 
+        | Unlinked -> acc 
         | Linked i -> 
             let old = try Link.find i acc with Not_found -> [] in
             Link.add i (k::old) acc)
-    lnk Link.empty
+    Link.empty
+
+
+
+
+
+(** {1 Utilities for merging} *)
 
+let ind1name = id_of_string "__ind1"
+let ind2name = id_of_string "__ind2"
 
+(** Performs verifications on two graphs before merging: they must not
+    be co-inductive, and for the moment they must not be mutual
+    either. *)
 let verify_inds mib1 mib2 =
-  if not mib1.mind_finite then Util.error "First argument is coinductive";
-  if not mib2.mind_finite then Util.error "Second argument is coinductive";
-  if mib1.mind_ntypes <> 1 then Util.error "First argument is mutual";
-  if mib2.mind_ntypes <> 1 then Util.error "Second argument is mutual";
+  if not mib1.mind_finite then error "First argument is coinductive";
+  if not mib2.mind_finite then error "Second argument is coinductive";
+  if mib1.mind_ntypes <> 1 then error "First argument is mutual";
+  if mib2.mind_ntypes <> 1 then error "Second argument is mutual";
   ()
 
+(** [apply_link lnk typ] returns the type [type] in which each
+     debruijn index linked in [lnk] has been lifted to its
+     correpsonding new index. *)
+let apply_link lnk typ = 
+  Link.fold 
+    (fun k x acc -> 
+      match x with
+        | Linked i -> substitterm 0 (mkRel k) (mkRel i) acc
+        | Unlinked -> acc) 
+    lnk typ 
+
+
+(** {1 Merging function graphs} *)
+
 (** [shift_linked_params mib1 mib2 lnk] Computes how many recursively
     uniform parameters of mutual inductives mib1 and mib2 remain
     uniform when linked by [lnk].
@@ -112,242 +337,422 @@ let verify_inds mib1 mib2 =
    Problem is, if some rec unif params are linked to non rec unif
    ones, they become non rec (and the following too). This function
    computes how many rec unif params we get from both inductives. *)
-let shift_linked_params mib1 mib2 lnk =
-  let linked_targets = revlinked lnk in
-  let is_param_of_mib2 x = 
-    x >= mib1.mind_nparams && x - mib1.mind_nparams < mib2.mind_nparams_rec in
-  let is_param_of_mib2 x = 
-    x >= mib1.mind_nparams && x - mib1.mind_nparams < mib2.mind_nparams_rec in
-  let i = ref 0 in
-  let found = ref false in
-  while !i < mib1.mind_nparams_rec && not !found do 
-    let linked = try Link.find !i linked_targets with Not_found -> [] in
-    if List.exists (fun x -> not (is_param_of_mib2 x)) linked then found := true;
-    i:=!i+1;
-  done; (* i should be (fst unparam or last rec param) + 1 (starting from 0) *)
-  let n_params1,n_unparams1 = 
-    if !found then !i-1,mib1.mind_nparams_rec+1-(!i) else mib1.mind_nparams_rec,0 in
-  i:=mib1.mind_nparams;
-  found := false;
-  while !i < mib1.mind_nparams + mib2.mind_nparams_rec && not !found do 
-    let linked = try Link.find !i lnk with Not_found -> assert false in
-    (match linked with
-      | Linked k -> if not (is_param_of_mib2 k) then found := true
-      | Unlinked _ -> ());
-    i:=!i+1;
-  done;
-  let n_params2,n_unparams2 = 
-    if not !found then mib2.mind_nparams_rec, 0
-    else
-      let unp = mib1.mind_nparams_rec + mib2.mind_nparams_rec - !i + 1 in
-      mib2.mind_nparams_rec - unp , unp in
-  { nprm1=n_params1; nuprm1=n_unparams1; nprm2=n_params2; nuprm2=n_unparams2}
-
-
-
-let rec listmapsome f l = 
-  match l with
-    | [] -> []
-    | e::l' -> 
-        match f e with
-          | None -> listmapsome f l'
-          | Some res -> res::listmapsome f l'
-
-
-let apply_link lnk typ = 
-  Link.fold 
-    (fun k x acc -> 
-      match x with
-        | Linked i -> substitterm 0 (mkRel k) (mkRel i) acc
-        | Unlinked _ -> acc) 
-    lnk typ 
+let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array) id =
+  let linked_targets = revlinked lnk2 in
+  let is_param_of_mib1 x = x < mib1.mind_nparams_rec in
+  let is_param_of_mib2 x = x < mib2.mind_nparams_rec in
+  let is_targetted_by_non_recparam_lnk1 i = 
+    try 
+      let targets = Link.find i linked_targets in 
+      List.exists (fun x -> not (is_param_of_mib2 x)) targets
+    with Not_found -> false in
+  let mlnk1 = 
+    Array.mapi
+      (fun i lkv -> 
+        let isprm = is_param_of_mib1 i in
+        let prmlost = is_targetted_by_non_recparam_lnk1 i in
+        match isprm , prmlost with
+          | true , true -> Prm_arg i (* recparam becoming ordinary *)
+          | true , false -> Prm_stable i (* recparam remains recparam*)
+          | false , _ -> Arg_stable i) (* Args of lnk1 are not linked *)
+      lnk1 in
+  let mlnk2 = 
+    Array.mapi
+      (fun i lkv -> 
+        let isprm = is_param_of_mib2 i in
+        (* FIXME: should use mlnk1.(i) instead of lnk2.(i) *)
+        match isprm , lnk2.(i) with
+          | true , Linked j when not (is_param_of_mib1 j) -> 
+              Prm_arg j (* recparam becoming ordinary *)
+          | true , Linked j -> Prm_linked j (*recparam linked to recparam*)
+          | true , Unlinked -> Prm_stable i (* recparam remains recparam*)
+          | false , Linked j -> Arg_linked j (* Args of lnk2 lost *)
+          | false , Unlinked -> Arg_stable i) (* Args of lnk2 remains *)
+      lnk2 in
+  let oib1 = mib1.mind_packets.(0) in
+  let oib2 = mib2.mind_packets.(0) in
+  (* count params remaining params *)
+  let n_params1 = array_prfx mlnk1 (fun i x -> not (mrgarg_stblparm x)) in
+  let n_params2 = array_prfx mlnk2 (fun i x -> not (mrgarg_stblparm x)) in
+
+  let recprms1,otherprms1 = 
+    list_fold_lefti
+      (fun i (acc1,acc2) x -> 
+        match mlnk1.(i) with
+          | Prm_stable _ -> x::acc1 , acc2 
+          | Prm_arg _ | Arg_stable _ -> acc1 , x::acc2 
+          | _ -> acc1 , acc2) (* Prm_linked and Arg_xxx = forget it *)
+      ([],[])
+      (List.rev oib1.mind_arity_ctxt)
+  in
+  let recprms2,otherprms2 = 
+    list_fold_lefti
+      (fun i (acc1,acc2) x -> 
+        match mlnk2.(i) with
+          | Prm_stable _ -> x::acc1 , acc2 
+          | Prm_arg _ | Arg_stable _ -> acc1 , x::acc2 
+          | _ -> acc1 , acc2) (* Prm_linked and Arg_xxx = forget it *)
+      ([],[])
+      (List.rev oib2.mind_arity_ctxt)
+  in
+  
+  {
+    ident=id;
+    mib1=mib1;
+    oib1 = oib1;
+    mib2=mib2;
+    oib2 = oib2;
+    lnk1 = mlnk1;
+    lnk2 = mlnk2;
+    nrecprms1 = n_params1;
+    recprms1 = recprms1;
+    otherprms1 = otherprms1;
+    notherprms1 = Array.length mlnk1 - n_params1;
+    nrecprms2 = n_params2;
+    recprms2 = recprms2;
+    otherprms2 = otherprms2;
+    notherprms2 = Array.length mlnk2 - n_params2;
+  }
 
-let ind1name = "__ind1"
-let ind2name = "__ind2"
-let newindname = "__newind"
-(* Operations on names *)
-let id_of_name = function
-    Anonymous -> id_of_string "H"
-  | Name id   -> id;;
-let name_of_string str = Name (id_of_string str)
-let string_of_name nme = string_of_id (id_of_name nme)
 
 
-let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl
 
-let isAppf f x = 
-  try
-    let _ = Printf.printf "isreccall %s\n" (string_of_id (destVar x) ) in
-    string_of_id (destVar x) = f with _ -> false
+(** {1 Merging functions} *)
 
 exception NoMerge
 
-let merge_app c1 c2 id1 id2 newid = 
-  match kind_of_term c1 , kind_of_term c2 with
-    | App(f1, arr1), App(f2,arr2) 
-        when isAppf id1 f1 && isAppf id2 f2 -> 
-        mkApp (mkVar (id_of_string newid) , Array.append arr1 arr2)
-    | App(f1, arr1), App(f2,arr2)  -> 
-        let _ = Printf.printf "id1 = %s ; id1 = %s" id1 id2 in
-        let _ = Tacinvutils.prNamedConstr "f1" f1 in
-        let _ = Tacinvutils.prNamedConstr "f2" f2 in
-        raise NoMerge
-    | _ -> 
-        let _ = Printf.printf "Not an App" in
-        raise NoMerge
-
-
-let rec merge_rec_hyps accrec ltyp =
+(* lnk is an link array of *all* args (from 1 and 2) *)
+let merge_app c1 c2 id1 id2 newid shift = 
+  let lnk = Array.append shift.lnk1 shift.lnk2 in
+  match c1 , c2 with
+    | RApp(_,f1, arr1), RApp(_,f2,arr2) 
+        when isVarf id1 f1 && isVarf id2 f2 -> 
+        let args = filter_shift lnk (arr1 @ arr2) in
+        RApp (dummy_loc,RVar (dummy_loc,newid) , 
+             args)
+    | RApp(_,f1, arr1), RApp(_,f2,arr2)  -> raise NoMerge
+    | _ -> raise NoMerge
+
+let merge_app_unsafe c1 c2 newid shift = 
+  let lnk = Array.append shift.lnk1 shift.lnk2 in
+  match c1 , c2 with
+    | RApp(_,f1, arr1), RApp(_,f2,arr2) -> 
+        let args = filter_shift lnk (arr1 @ arr2) in
+        RApp (dummy_loc,RVar(dummy_loc,newid) , args)
+    | _ -> raise NoMerge
+
+let onefoud = ref false
+
+let rec merge_rec_hyps_aux shift accrec (ltyp:(Names.name * Rawterm.rawconstr) list) =
   match ltyp with
     | [] -> []
     | (nme,t) as e ::lt -> 
-        match kind_of_term t with
-          | App(f, arr) when isAppf ind2name f -> 
+        match t with
+          | RApp(_,f, largs) when isVarf ind2name f ->               
+              let _ = onefoud := true in
               let rechyps = 
                 List.map 
                   (fun (nme,ind) -> 
-                  match kind_of_term ind with
-                    | App(i,args) -> 
-                        nme, 
-                        mkApp(mkVar(id_of_string newindname), (Array.append args arr))
-                    | _ -> assert false)
+                    match ind with
+                      | RApp(_,i,args) -> 
+                          let newargs = 
+                            filter_shift (Array.append shift.lnk1 shift.lnk2) (args@largs)  in
+                          nme, RApp(dummy_loc,RVar(dummy_loc,shift.ident), newargs)
+                      | _ -> assert false)
                   accrec in
-              let nhyps = List.length rechyps in
-              (List.fold_left (fun acc x -> x :: lift_ldecl 1 acc) [] rechyps)
-              @ merge_rec_hyps (lift_ldecl nhyps accrec) (lift_ldecl nhyps lt)
-          | _ -> e :: merge_rec_hyps (lift_ldecl 1 accrec) lt
-              
-
-let rec merge_types accrec1 (ltyp1:(name * constr) list)
-    concl1 (ltyp2:(name * constr) list) concl2: (name * constr) list * constr = 
+              rechyps @ merge_rec_hyps_aux shift accrec lt
+          | _ -> e :: merge_rec_hyps_aux shift accrec lt
+
+
+let merge_rec_hyps shift accrec (ltyp:(Names.name * Rawterm.rawconstr) list) =
+  let l = merge_rec_hyps_aux shift accrec ltyp in
+  l
+
+let rec build_suppl_reccall nme (accrec:(name * rawconstr) list) concl2 shift = 
+  List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 nme shift)) accrec
+
+
+
+(* 
+  match accrec with
+    | [] -> []
+    | (nm,tp)::l -> (nm,merge_app_unsafe tp concl2 nme lnk) 
+        :: build_suppl_reccall nme l concl2 shift
+ *)
+
+
+
+
+let rec merge_types shift accrec1 (ltyp1:(name * rawconstr) list)
+    concl1 (ltyp2:(name * rawconstr) list) concl2
+    : (name * rawconstr) list * rawconstr = 
   let res = 
   match ltyp1 with
     | [] -> 
-        let rechyps = merge_rec_hyps accrec1 ltyp2 in
-        let suppl_hyps = List.length rechyps - List.length ltyp2 in
-        rechyps 
-          , merge_app (lift (List.length rechyps) concl1) (lift suppl_hyps concl2) 
-            ind1name ind2name newindname
+        let _ = onefoud := false in
+        let rechyps =(*If accrec1 is empty, use conlusion instead of accrec1 
+                       to merge rec calls*)
+          merge_rec_hyps shift
+            (if accrec1<>[] then accrec1 else [name_of_string "concl1",concl1])
+            ltyp2 in
+        (* If no reccalls has been found in ltyp2 and accrec1 is not
+           empty, create one with accrec1 + concl2  *)
+        let suppl_rechyps = 
+          if accrec1 = [] || !onefoud then []
+          else build_suppl_reccall shift.ident accrec1 concl2 shift in
+        rechyps @ suppl_rechyps
+          , merge_app concl1 concl2 ind1name ind2name shift.ident shift
     | (nme,t1)as e ::lt1 -> 
-        match kind_of_term t1 with
-          | App(f,carr) when isAppf ind1name f -> 
-              merge_types (e::accrec1) (lift_ldecl (-1) lt1)
-                (lift (-1) concl1) ltyp2 concl2
+        match t1 with
+          | RApp(_,f,carr) when isVarf ind1name f -> 
+              merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2
           | _ -> 
               let recres, recconcl2 =
-                merge_types (lift_ldecl 1 accrec1) lt1 concl1 ltyp2 concl2 in
+                merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in
               ((nme,t1) :: recres) , recconcl2
   in
   res
 
 
-(* Return a type if the 2 constructors are not incompatible *)
-let merge_one_constructor lnk shift (typcstr1:types) (typcstr2:types):types list =
-  let prms1,rest1 = decompose_prod_n shift.nprm1 typcstr1 in
-  let prms2,rest2 = decompose_prod_n shift.nprm2 typcstr2 in
-  let newlnk = liftlink shift.nprm1 lnk in
-  let hyps1,concl1 = decompose_prod (lift shift.nprm2 rest1) in
-  let hyps2,concl2' = decompose_prod (apply_link newlnk rest2) in
-  let ltyp,concl2 = merge_types [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in
-  let typ = compose_prod (List.rev ltyp) concl2 (* FIXME *) in
-  
-  let _ = Tacinvutils.prNamedConstr "rest1 = " rest1 in
-  let _ = Tacinvutils.prNamedConstr "rest2 = " rest2 in
-  let _ = Tacinvutils.prNamedConstr "TYP" typ in
-  let typwithprms = compose_prod (prms1@prms2) typ in
-  let _ = Tacinvutils.prNamedConstr "TYPWTHP" typwithprms in
-  let _ = print_string "\n***\n" in
-  [typwithprms]
-
-let rec merge_constructors lnk shift (typcstr1:types list) (typcstr2:types list) =
+(** [build_link_map_aux allargs1 allargs2 shift] returns the mapping of
+    linked args [allargs2] to target args of [allargs1] as specified
+    in [shift]. [allargs1] and [allargs2] are in reverse order.  Also
+    returns the list of unlinked vars of [allargs2]. *)
+let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array)
+    (lnk:int merged_arg array) =
+  array_fold_lefti
+    (fun i acc e -> 
+      if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *)
+      else 
+        match e with 
+          | Prm_linked j | Arg_linked j -> Idmap.add allargs2.(i) allargs1.(j) acc
+          | _ -> acc)
+    Idmap.empty lnk
+
+let build_link_map allargs1 allargs2 lnk =
+  let allargs1 =
+    Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs1)) in
+  let allargs2 =
+    Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs2)) in
+  build_link_map_aux allargs1 allargs2 lnk
+
+
+(** [merge_one_constructor lnk shift typcstr1 typcstr2] merges the two
+    constructor rawtypes [typcstr1] and [typcstr2].  [typcstr1] and
+    [typcstr2] contain all parameters (including rec. unif. ones) of
+    their inductive.
+
+    if  [typcstr1] and [typcstr2] are of the form:
+
+    forall recparams1, forall ordparams1, H1a -> H2a... (I1 x1 y1 ... z1)
+    forall recparams2, forall ordparams2, H2b -> H2b... (I2 x2 y2 ... z2)
+
+    we build:
+
+    forall recparams1 (recparams2 without linked params),
+     forall ordparams1 (ordparams2 without linked params),
+      H1a' -> H2a' -> ...  -> H2a' -> H2b' -> ... 
+        -> (newI x1 ... z1 x2 y2 ...z2 without linked params)
+
+    where Hix' have been adapted, ie: 
+      - linked vars have been changed,
+      - rec calls to I1 and I2 have been replaced by rec calls to
+        newI. More precisely calls to I1 and I2 have been merge by an
+        experimental heuristic (in particular if n o rec calls for I1
+        or I2 is found, we use the conclusion as a rec call). See
+        [merge_types] above.
+
+    Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint.
+
+    TODO: return nothing if equalities (after linking) are contradictory. *)
+let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
+    (typcstr2:rawconstr) : rawconstr * (name * rawconstr) list =
+  (* -1 because last arg is functional result ?? *)
+  (* FIXME: les nomes des parametres corerspondent en principe au
+     parametres du niveau mib, mais il faudrait s'en assurer *)
+  let nargs1 = shift.mib1.mind_nparams + shift.oib1.mind_nrealargs -1 in
+  let nargs2 = shift.mib2.mind_nparams + shift.oib2.mind_nrealargs -1 in
+  let allargs1,rest1 = raw_decompose_prod_n nargs1 typcstr1 in
+  let allargs2,rest2 = raw_decompose_prod_n nargs2 typcstr2 in  
+  (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *)
+  let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in
+  let allargs2_filtered = 
+    let lnk2nofunc,_ = list_chop (Array.length shift.lnk2 -1) 
+      (Array.to_list shift.lnk2) in
+    let comb = List.combine allargs2 lnk2nofunc in
+    let combres = List.filter (fun (arg,mrg) -> not (mrgarg_linked mrg)) comb in
+    fst (List.split combres) in
+  let rest2 = change_vars linked_map rest2 in
+  let hyps1,concl1 = raw_decompose_prod rest1 in
+  let hyps2,concl2' = raw_decompose_prod rest2 in
+  let ltyp,concl2 = merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in
+  let typ = raw_compose_prod concl2 (List.rev ltyp) in
+  let args1 , params1 = list_chop_end shift.nrecprms1 allargs1 in
+  let args2 , params2 = list_chop_end shift.nrecprms2 allargs2_filtered in
+  let typwithprms = raw_compose_prod typ (args2@args1) in
+  typwithprms , (params2@params1) (* useless *)
+
+let merge_constructor_id id1 id2:identifier = 
+  let s1 = string_of_id id1 in
+  let s2 = string_of_id id2 in
+  id_of_string (s1^s2)
+
+(** [merge_constructors lnk shift avoid] merges the two list of
+    constructor [(name*type)]. These are translated to rawterms
+    first, each of them having distinct var names. *)
+let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
+    (typcstr1:(identifier * types) list) 
+    (typcstr2:(identifier * types) list) : (identifier * rawconstr) list =
   List.flatten 
     (List.map
-        (fun typ1 -> 
+        (fun (id1,typ1) -> 
+          let typ1 = substitterm 0 (mkRel 1) (mkVar ind1name) typ1 in
+          let rawtyp1 = Detyping.detype false (Idset.elements avoid) [] typ1 in
+          let idsoftyp1:Idset.t = ids_of_rawterm rawtyp1 in
           List.map
-            (fun typ2 -> 
-              let typ1 =
-                substitterm 0 (mkRel 1) (mkVar (id_of_string ind1name)) typ1 in
-              let typ2 =
-                substitterm 0 (mkRel 1) (mkVar (id_of_string ind2name)) typ2 in
-              let _ = Tacinvutils.prNamedConstr "Whole typ1 = " typ1 in
-              let _ = Tacinvutils.prNamedConstr "Wholetyp2 = " typ2 in
-              let _ = print_string "\n\n" in
-              merge_one_constructor lnk shift typ1 typ2)
-            typcstr2) 
-        typcstr1) 
+            (fun (id2,typ2) -> 
+              let typ2 = substitterm 0 (mkRel 1) (mkVar ind2name) typ2 in
+              (* Avoid also rawtyp1 names *)
+              let avoid2 = Idset.union avoid idsoftyp1 in
+              let rawtyp2 = Detyping.detype false (Idset.elements avoid2) [] typ2 in
+              let typ,params = merge_one_constructor shift rawtyp1 rawtyp2 in
+              let newcstror_id = merge_constructor_id id1 id2 in
+              newcstror_id , typ)
+            typcstr2)
+        typcstr1)
     
-let rec merge_inductive_body (lnk: linked_var Link.t) (shift:int shifted_params)
-    (oib1:one_inductive_body) (oib2:one_inductive_body)  =
+(** [merge_inductive_body lnk shift avoid oib1 oib2] merges two
+    inductive bodies [oib1] and [oib2], linking with [lnk], params
+    info in [shift], avoiding identifiers in [avoid]. *)
+let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
+    (oib2:one_inductive_body) : (identifier * rawconstr) list =
   let lcstr1 = Array.to_list oib1.mind_user_lc in
   let lcstr2 = Array.to_list oib2.mind_user_lc in
-  let types_of_cstrs = merge_constructors lnk shift lcstr1 lcstr2 in
-  ()
+  let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
+  let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in
+  let newshift = shift (* { shift with
+    nargs1 = oib1.mind_nrealargs;
+    nargs2 = oib2.mind_nrealargs; } *) in
+  let res = merge_constructors newshift avoid lcstr1 lcstr2 in
+  res
 
-let rec merge_mutual_inductive_body (lnk: linked_var Link.t)
+(** [build_raw_params prms_decl avoid] returns a list of variables
+    attributed to the list of decl [prms_decl], avoiding names in
+    [avoid]. *)
+let build_raw_params prms_decl avoid =
+  let dummy_constr = compose_prod prms_decl mkProp in
+  let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in
+  let res,_ = raw_decompose_prod dummy_rawconstr in
+  res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr)))
+
+(** [merge_mutual_inductive_body lnk mib1 mib2 shift] merge mutual
+    inductive bodies [mib1] and [mib2] linking vars with
+    [lnk]. [shift] information on parameters of the new inductive.
+    For the moment, inductives are supposed to be non mutual.
+*)
+let rec merge_mutual_inductive_body
     (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) 
-    (shift:int shifted_params) =
-  merge_inductive_body lnk shift mib1.mind_packets.(0) mib2.mind_packets.(0) 
+    (shift:merge_infos) =
+  (* Mutual not treated, we take first ind body of each. *)
+  let nprms1 = mib1.mind_nparams_rec in (* n# of rec uniform parms of mib1 *)
+  let prms1 = (* rec uniform parms of mib1 *)
+    List.map (fun (x,_,y) -> x,y) (fst (list_chop nprms1 mib1.mind_params_ctxt)) in
 
+  (* useless: *)
+  let prms1_named,avoid' = build_raw_params prms1 [] in
+  let prms2_named,avoid = build_raw_params prms1 avoid' in
+  let avoid:Idset.t = List.fold_right Idset.add avoid Idset.empty in  
+  (* *** *)
 
+  merge_inductive_body shift avoid mib1.mind_packets.(0) mib2.mind_packets.(0) 
 
+  
+
+(* TODO: Define and use everywhere needed a function [is_linked i lnk] *)
+(* TODO: Define and use everywhere needed a function List.filteri,
+   List.fold_lefti... Probably with a initial int for the counter. *)
+let merge_rec_params_and_arity params1 params2 shift (concl:constr) = 
+  let params = shift.recprms1 @ shift.recprms2 in
+  let resparams, _ =
+    List.fold_left
+      (fun (acc,env) (nme,_,tp) -> 
+        let typ = Constrextern.extern_constr false env tp in
+        let newenv = Environ.push_rel (nme,None,tp) env in
+        LocalRawAssum ([(dummy_loc,nme)] , typ) :: acc , newenv)
+      ([],Global.env())
+      params in
+  let concl = Constrextern.extern_constr false (Global.env()) concl in
+  let arity,_ = 
+    List.fold_left 
+      (fun (acc,env) (nm,_,c) -> 
+        let typ = Constrextern.extern_constr false env c in
+        let newenv = Environ.push_rel (nm,None,c) env in
+        CProdN (dummy_loc, [[(dummy_loc,nm)],typ] , acc) , newenv)
+      (concl,Global.env())
+      (shift.otherprms1@shift.otherprms2) in  
+  resparams,arity
+
+  
 
-let merge_inductive (ind1: inductive) (ind2: inductive) (lnk: linked_var Link.t) =
+(** [rawterm_list_to_inductive_expr ident rawlist] returns the
+    induct_expr corresponding to the the list of constructor types
+    [rawlist], named ident.
+    FIXME: params et cstr_expr (arity) *)
+let rawterm_list_to_inductive_expr mib1 mib2 shift
+    (rawlist:(identifier * rawconstr) list):inductive_expr =
+  let rawterm_to_constr_expr = (* build a constr_expr from a rawconstr *)
+    Options.with_option Options.raw_print (Constrextern.extern_rawtype Idset.empty) in
+  let lident = dummy_loc, shift.ident in
+  let bindlist , cstr_expr = (* params , arities  , FIXME: verify this *)
+    merge_rec_params_and_arity 
+      mib1.mind_params_ctxt mib2.mind_params_ctxt shift mkSet in
+  let cstor_cpt = ref 0 in
+  let bld_cor_name id =
+    cstor_cpt := !cstor_cpt + 1;
+    id_of_string (string_of_id id ^ string_of_int !cstor_cpt) in
+  let lcstor_expr : (bool * (lident * constr_expr)) list  = 
+    List.map (* zeta_normalize t ? *)
+      (fun (id,t) -> false, ((dummy_loc,bld_cor_name id),rawterm_to_constr_expr t))
+      rawlist in  
+  lident , bindlist , cstr_expr , lcstor_expr
+
+(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking
+    variables specified in [lnk]. Graphs are not supposed to be mutual
+    inductives for the moment. *)
+let merge_inductive (ind1: inductive) (ind2: inductive) 
+    (lnk1: linked_var array) (lnk2: linked_var array) id =
   let env = Global.env() in
-  let mib1,ib1 = Inductive.lookup_mind_specif env ind1 in
-  let mib2,ib2 = Inductive.lookup_mind_specif env ind2 in
-  let _ = verify_inds mib1 mib2 in
-  let shift_prm = shift_linked_params mib1 mib2 lnk in
-  merge_mutual_inductive_body lnk mib1 mib2 shift_prm
+  let mib1,_ = Inductive.lookup_mind_specif env ind1 in
+  let mib2,_ = Inductive.lookup_mind_specif env ind2 in
+  let _ = verify_inds mib1 mib2 in (* raises an exception if something wrong *)
+  (* compute params that become ordinary args (because linked to ord. args) *)
+  let shift_prm = shift_linked_params mib1 mib2 lnk1 lnk2 id in
+  let rawlist:(identifier * rawconstr) list = 
+    merge_mutual_inductive_body mib1 mib2 shift_prm in
+  let indexpr = rawterm_list_to_inductive_expr mib1 mib2 shift_prm rawlist in
+  (* Declare inductive *)
+  Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
 
 
-let merge (cstr1:constr) (cstr2:constr) (args1:constr array) (args2:constr array) =
+
+let merge (cstr1:constr) (cstr2:constr) (args1:constr array) (args2:constr array) id =
   let env = Global.env() in
   let ind1,_cstrlist1 = Inductiveops.find_inductive env Evd.empty cstr1 in
   let ind2,_cstrlist2 = Inductiveops.find_inductive env Evd.empty cstr2 in
-  let arrmem arr e = 
-    let x = ref 0 in
-    let found = ref false in
-    while not !found & !x < Array.length arr do
-      if arr.(!x)=e then found := true else x:=!x+1
-    done;
-    if not !found  then None else Some !x in
-  let i = ref (-1) in
-  let lnk_partial = 
-    Array.fold_left (fun acc c -> i:=!i+1; Link.add !i (Unlinked !i) acc) Link.empty args2 in
-  let ilinked = ref !i in
-  let lnk_all = 
-    Array.fold_left (
-        fun acc c -> 
-          match arrmem args1 c with
-            | Some j -> i:=!i+1;Link.add !i (Linked j) acc
-            | None -> i:=!i+1; ilinked:=!ilinked+1;Link.add !i (Unlinked !ilinked) acc)
-      lnk_partial args2 in
-(*  let _ = print_string "\n\n Links =      " in
-  let _ = Link.iter (fun k e -> Printf.printf "%d -> %s, " k (prlinked e)) lnk_all in *)
-  merge_inductive ind1 ind2 lnk_all
+  let lnk1 = (* args1 are unlinked. FIXME? mergescheme (G x x) ?? *)
+    Array.mapi (fun i c -> Unlinked) args1 in
+  let lnk2 = (* args2 may be linked to args1 members. FIXME: same 
+                   as above: vars may be linked inside args2?? *)
+    Array.mapi
+      (fun i c -> 
+        match array_find args1 (fun i x -> x=c) with
+          | Some j -> (Linked j)
+          | None -> Unlinked) 
+      args2 in
+  let resa = merge_inductive ind1 ind2 lnk1 lnk2 id in
+  resa
 
-let id_of_name = function
-    Anonymous -> id_of_string "H"
-  | Name id   -> id;;
-let string_of_name nme = string_of_id (id_of_name nme)
 
-let showind (id:identifier) =
-  let cstrid = Tacinterp.constr_of_id (Global.env()) id in
-  let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
-  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
-  List.iter (fun (nm, optcstr, tp) -> 
-    print_string (string_of_name nm^":");
-    Tacinvutils.prconstr tp; print_string "\n") 
-    ib1.mind_arity_ctxt;
-  (match ib1.mind_arity with
-    | Monomorphic x ->
-        Printf.printf "arity :"; Tacinvutils.prconstr x.mind_user_arity
-    | Polymorphic x -> 
-        Printf.printf "arity : universe?");
-  Array.iteri 
-    (fun i x -> Printf.printf"type constr %d :" i ; Tacinvutils.prconstr x)
-    ib1.mind_user_lc
-;;
 
 
 
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index a0655d858..ed46ec72d 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -35,6 +35,18 @@ let raw_decompose_prod =
 let raw_compose_prod = 
   List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
 
+let raw_decompose_prod_n n = 
+  let rec raw_decompose_prod i args c = 
+    if i<=0 then args,c
+    else
+      match c with
+	| RProd(_,n,t,b) -> 
+	    raw_decompose_prod (i-1) ((n,t)::args) b 
+	| rt -> args,rt
+  in
+  raw_decompose_prod n []
+
+
 let raw_decompose_app = 
   let rec decompose_rapp acc rt =
 (*     msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *)
@@ -527,6 +539,33 @@ let ids_of_pat =
   in
   ids_of_pat Idset.empty 
   
+let id_of_name = function 
+  | Names.Anonymous -> id_of_string "x" 
+  | Names.Name x -> x
+
+(* TODO: finish Rec caes *)
+let ids_of_rawterm c = 
+  let rec ids_of_rawterm acc c = 
+    let idof = id_of_name in
+    match c with
+      | RVar (_,id) -> id::acc
+      | RApp (loc,g,args) -> 
+          ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
+      | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
+      | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+      | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
+      | RLetTuple (_,nal,(na,po),b,c) -> 
+          List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
+      | RCases (loc,rtntypopt,tml,brchl) -> 
+	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
+      | RRec _ -> failwith "Fix inside a constructor branch"
+      | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> []
+  in
+  (* build the set *)
+  List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c)
+  
 
 
 
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 7cf7a0eb2..9647640cf 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -31,6 +31,7 @@ val mkRCast : rawconstr* rawconstr -> rawconstr
   These are analogous to the ones constrs
 *)
 val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr
+val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr
 val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list  ->  rawconstr 
 val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
 
@@ -107,6 +108,8 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
 *)
 val   ids_of_pat : cases_pattern -> Names.Idset.t 
 
+(* TODO: finish this function (Fix not treated) *)
+val ids_of_rawterm: rawconstr -> Names.Idset.t
 
 (* 
    removing let_in construction in a rawterm