Merge PR #11776: [ocamlformat] Enable for funind.

Reviewed-by: Matafou
Ack-by: Zimmi48
Ack-by: maximedenes

1 files changed, 1199 insertions, 1188 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e08ad9af3a..11e4fa0ac7 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -10,34 +10,27 @@ open Indfun_common
 open CErrors
 open Util
 open Glob_termops
-
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-let observe strm =
-  if do_observe ()
-  then Feedback.msg_debug strm
-  else ()
+let observe strm = if do_observe () then Feedback.msg_debug strm else ()
+
 (*let observennl strm =
   if do_observe ()
   then Pp.msg strm
   else ()*)
 
-
-type binder_type =
-  | Lambda of Name.t
-  | Prod of Name.t
-  | LetIn of Name.t
-
-type glob_context = (binder_type*glob_constr) list
-
+type binder_type = Lambda of Name.t | Prod of Name.t | LetIn of Name.t
+type glob_context = (binder_type * glob_constr) list
 
 let rec solve_trivial_holes pat_as_term e =
-  match DAst.get pat_as_term, DAst.get e with
-  | GHole _,_ -> e
-  | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe ->
-       DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
-  | _,_ -> pat_as_term
+  match (DAst.get pat_as_term, DAst.get e) with
+  | GHole _, _ -> e
+  | GApp (fp, argsp), GApp (fe, argse) when glob_constr_eq fp fe ->
+    DAst.make
+      (GApp
+         (solve_trivial_holes fp fe, List.map2 solve_trivial_holes argsp argse))
+  | _, _ -> pat_as_term
 
 (*
    compose_glob_context [(bt_1,n_1,t_1);......] rt returns
@@ -45,31 +38,26 @@ let rec solve_trivial_holes pat_as_term e =
    binders corresponding to the bt_i's
 *)
 let compose_glob_context =
-  let compose_binder  (bt,t) acc =
+  let compose_binder (bt, t) acc =
     match bt with
-      | Lambda n -> mkGLambda(n,t,acc)
-      | Prod n -> mkGProd(n,t,acc)
-      | LetIn n -> mkGLetIn(n,t,None,acc)
+    | Lambda n -> mkGLambda (n, t, acc)
+    | Prod n -> mkGProd (n, t, acc)
+    | LetIn n -> mkGLetIn (n, t, None, acc)
   in
   List.fold_right compose_binder
 
-
 (*
    The main part deals with building a list of globalized constructor expressions
    from the rhs of a fixpoint equation.
 *)
 
 type 'a build_entry_pre_return =
-    {
-      context : glob_context;  (* the binding context of the result *)
-      value : 'a; (* The value *)
-    }
+  { context : glob_context
+  ; (* the binding context of the result *)
+    value : 'a (* The value *) }
 
 type 'a build_entry_return =
-    {
-      result : 'a build_entry_pre_return list;
-      to_avoid : Id.t list
-    }
+  {result : 'a build_entry_pre_return list; to_avoid : Id.t list}
 
 (*
   [combine_results combine_fun res1 res2] combine two results [res1] and [res2]
@@ -81,64 +69,55 @@ type 'a build_entry_return =
 *)
 
 let combine_results
-    (combine_fun : 'a build_entry_pre_return -> 'b build_entry_pre_return ->
-      'c build_entry_pre_return
-    )
-    (res1: 'a build_entry_return)
-    (res2 : 'b build_entry_return)
-    : 'c build_entry_return
-    =
-  let pre_result =     List.map
-    ( fun res1 ->  (* for each result in arg_res *)
-          List.map (* we add it in each args_res *)
-            (fun res2 ->
-               combine_fun res1 res2
-            )
-            res2.result
-      )
+    (combine_fun :
+         'a build_entry_pre_return
+      -> 'b build_entry_pre_return
+      -> 'c build_entry_pre_return) (res1 : 'a build_entry_return)
+    (res2 : 'b build_entry_return) : 'c build_entry_return =
+  let pre_result =
+    List.map
+      (fun res1 ->
+        (* for each result in arg_res *)
+        List.map (* we add it in each args_res *)
+          (fun res2 -> combine_fun res1 res2)
+          res2.result)
       res1.result
-  in (* and then we flatten the map *)
-  {
-    result = List.concat pre_result;
-    to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid
-  }
-
+  in
+  (* and then we flatten the map *)
+  { result = List.concat pre_result
+  ; to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid }
 
 (*
    The combination function for an argument with a list of argument
 *)
 
 let combine_args arg args =
-  {
-    context = arg.context@args.context;
-    (* Note that the binding context of [arg] MUST be placed before the one of
+  { context = arg.context @ args.context
+  ; (* Note that the binding context of [arg] MUST be placed before the one of
        [args] in order to preserve possible type dependencies
     *)
-    value = arg.value::args.value;
-  }
+    value = arg.value :: args.value }
 
-
-let ids_of_binder =  function
+let ids_of_binder = function
   | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty
-  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id
+  | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id
 
 let rec change_vars_in_binder mapping = function
-    [] -> []
-  | (bt,t)::l ->
-      let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in
-      (bt,change_vars mapping t)::
-        (if Id.Map.is_empty new_mapping
-         then l
-         else change_vars_in_binder new_mapping l
-        )
+  | [] -> []
+  | (bt, t) :: l ->
+    let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in
+    (bt, change_vars mapping t)
+    ::
+    ( if Id.Map.is_empty new_mapping then l
+    else change_vars_in_binder new_mapping l )
 
 let rec replace_var_by_term_in_binder x_id term = function
   | [] -> []
-  | (bt,t)::l ->
-      (bt,replace_var_by_term x_id term t)::
-        if Id.Set.mem x_id (ids_of_binder bt)
-        then l
-        else replace_var_by_term_in_binder x_id term l
+  | (bt, t) :: l ->
+    (bt, replace_var_by_term x_id term t)
+    ::
+    ( if Id.Set.mem x_id (ids_of_binder bt) then l
+    else replace_var_by_term_in_binder x_id term l )
 
 let add_bt_names bt = Id.Set.union (ids_of_binder bt)
 
@@ -146,128 +125,116 @@ let apply_args ctxt body args =
   let need_convert_id avoid id =
     List.exists (is_free_in id) args || Id.Set.mem id avoid
   in
-  let need_convert avoid  bt =
+  let need_convert avoid bt =
     Id.Set.exists (need_convert_id avoid) (ids_of_binder bt)
   in
-  let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.Set.t) =
+  let next_name_away (na : Name.t) (mapping : Id.t Id.Map.t) (avoid : Id.Set.t)
+      =
     match na with
-       | Name id when Id.Set.mem id avoid ->
-           let new_id = Namegen.next_ident_away id avoid in
-           Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid
-       | _ -> na,mapping,avoid
+    | Name id when Id.Set.mem id avoid ->
+      let new_id = Namegen.next_ident_away id avoid in
+      (Name new_id, Id.Map.add id new_id mapping, Id.Set.add new_id avoid)
+    | _ -> (na, mapping, avoid)
   in
-  let next_bt_away bt (avoid:Id.Set.t) =
+  let next_bt_away bt (avoid : Id.Set.t) =
     match bt with
-      | LetIn na ->
-          let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
-          LetIn new_na,mapping,new_avoid
-      | Prod na ->
-          let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
-          Prod new_na,mapping,new_avoid
-      | Lambda na ->
-          let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
-          Lambda new_na,mapping,new_avoid
+    | LetIn na ->
+      let new_na, mapping, new_avoid = next_name_away na Id.Map.empty avoid in
+      (LetIn new_na, mapping, new_avoid)
+    | Prod na ->
+      let new_na, mapping, new_avoid = next_name_away na Id.Map.empty avoid in
+      (Prod new_na, mapping, new_avoid)
+    | Lambda na ->
+      let new_na, mapping, new_avoid = next_name_away na Id.Map.empty avoid in
+      (Lambda new_na, mapping, new_avoid)
   in
   let rec do_apply avoid ctxt body args =
-    match ctxt,args with
-      | _,[] -> (* No more args *)
-          (ctxt,body)
-      | [],_ -> (* no more fun *)
-          let f,args' = glob_decompose_app body in
-          (ctxt,mkGApp(f,args'@args))
-      | (Lambda Anonymous,t)::ctxt',arg::args' ->
-          do_apply avoid ctxt' body args'
-      | (Lambda (Name id),t)::ctxt',arg::args' ->
-          let new_avoid,new_ctxt',new_body,new_id =
-            if need_convert_id avoid id
-            then
-              let new_avoid =  Id.Set.add id avoid in
-              let new_id = Namegen.next_ident_away id new_avoid in
-              let new_avoid' = Id.Set.add new_id new_avoid in
-              let mapping = Id.Map.add id new_id Id.Map.empty in
-              let new_ctxt' = change_vars_in_binder mapping ctxt' in
-              let new_body = change_vars mapping body in
-              new_avoid',new_ctxt',new_body,new_id
-            else
-              Id.Set.add id avoid,ctxt',body,id
-          in
-          let new_body = replace_var_by_term new_id arg new_body in
-          let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
-          do_apply avoid new_ctxt' new_body args'
-      | (bt,t)::ctxt',_ ->
-          let new_avoid,new_ctxt',new_body,new_bt =
-            let new_avoid = add_bt_names bt avoid in
-            if need_convert avoid bt
-            then
-              let new_bt,mapping,new_avoid = next_bt_away bt new_avoid in
-              (
-                new_avoid,
-                change_vars_in_binder mapping ctxt',
-                change_vars mapping body,
-                new_bt
-             )
-            else new_avoid,ctxt',body,bt
-          in
-          let new_ctxt',new_body =
-            do_apply new_avoid new_ctxt' new_body args
-          in
-          (new_bt,t)::new_ctxt',new_body
+    match (ctxt, args) with
+    | _, [] ->
+      (* No more args *)
+      (ctxt, body)
+    | [], _ ->
+      (* no more fun *)
+      let f, args' = glob_decompose_app body in
+      (ctxt, mkGApp (f, args' @ args))
+    | (Lambda Anonymous, t) :: ctxt', arg :: args' ->
+      do_apply avoid ctxt' body args'
+    | (Lambda (Name id), t) :: ctxt', arg :: args' ->
+      let new_avoid, new_ctxt', new_body, new_id =
+        if need_convert_id avoid id then
+          let new_avoid = Id.Set.add id avoid in
+          let new_id = Namegen.next_ident_away id new_avoid in
+          let new_avoid' = Id.Set.add new_id new_avoid in
+          let mapping = Id.Map.add id new_id Id.Map.empty in
+          let new_ctxt' = change_vars_in_binder mapping ctxt' in
+          let new_body = change_vars mapping body in
+          (new_avoid', new_ctxt', new_body, new_id)
+        else (Id.Set.add id avoid, ctxt', body, id)
+      in
+      let new_body = replace_var_by_term new_id arg new_body in
+      let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
+      do_apply avoid new_ctxt' new_body args'
+    | (bt, t) :: ctxt', _ ->
+      let new_avoid, new_ctxt', new_body, new_bt =
+        let new_avoid = add_bt_names bt avoid in
+        if need_convert avoid bt then
+          let new_bt, mapping, new_avoid = next_bt_away bt new_avoid in
+          ( new_avoid
+          , change_vars_in_binder mapping ctxt'
+          , change_vars mapping body
+          , new_bt )
+        else (new_avoid, ctxt', body, bt)
+      in
+      let new_ctxt', new_body = do_apply new_avoid new_ctxt' new_body args in
+      ((new_bt, t) :: new_ctxt', new_body)
   in
   do_apply Id.Set.empty ctxt body args
 
-
 let combine_app f args =
-  let new_ctxt,new_value = apply_args f.context f.value args.value in
-  {
-    (* Note that the binding context of [args] MUST be placed before the one of
+  let new_ctxt, new_value = apply_args f.context f.value args.value in
+  { (* Note that the binding context of [args] MUST be placed before the one of
        the applied value in order to preserve possible type dependencies
     *)
-      context = args.context@new_ctxt;
-      value = new_value;
-  }
+    context = args.context @ new_ctxt
+  ; value = new_value }
 
 let combine_lam n t b =
-  {
-    context = [];
-    value = mkGLambda(n, compose_glob_context t.context t.value,
-                      compose_glob_context b.context b.value )
-  }
+  { context = []
+  ; value =
+      mkGLambda
+        ( n
+        , compose_glob_context t.context t.value
+        , compose_glob_context b.context b.value ) }
 
 let combine_prod2 n t b =
-  {
-    context = [];
-    value = mkGProd(n, compose_glob_context t.context t.value,
-                      compose_glob_context b.context b.value )
-  }
+  { context = []
+  ; value =
+      mkGProd
+        ( n
+        , compose_glob_context t.context t.value
+        , compose_glob_context b.context b.value ) }
 
 let combine_prod n t b =
-  { context = t.context@((Prod n,t.value)::b.context); value = b.value}
+  {context = t.context @ ((Prod n, t.value) :: b.context); value = b.value}
 
 let combine_letin n t b =
-  { context = t.context@((LetIn n,t.value)::b.context); value = b.value}
-
+  {context = t.context @ ((LetIn n, t.value) :: b.context); value = b.value}
 
 let mk_result ctxt value avoid =
-  {
-    result =
-      [{context = ctxt;
-        value = value}]
-        ;
-    to_avoid = avoid
-  }
+  {result = [{context = ctxt; value}]; to_avoid = avoid}
+
 (*************************************************
   Some functions to deal with overlapping patterns
 **************************************************)
 
-let coq_True_ref  = lazy (Coqlib.lib_ref "core.True.type")
+let coq_True_ref = lazy (Coqlib.lib_ref "core.True.type")
 let coq_False_ref = lazy (Coqlib.lib_ref "core.False.type")
 
 (*
   [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
   (the list of expressions on which we will do the matching)
  *)
-let make_discr_match_el  =
-  List.map (fun e -> (e,(Anonymous,None)))
+let make_discr_match_el = List.map (fun e -> (e, (Anonymous, None)))
 
 (*
   [make_discr_match_brl i \[pat_1,...,pat_n\]]  constructs a discrimination pattern matching on the ith expression.
@@ -283,23 +250,21 @@ let make_discr_match_el  =
 *)
 let make_discr_match_brl i =
   List.map_i
-    (fun j {CAst.v=(idl,patl,_)} -> CAst.make @@
-       if Int.equal j i
-       then (idl,patl, mkGRef (Lazy.force coq_True_ref))
-       else (idl,patl, mkGRef (Lazy.force coq_False_ref))
-    )
+    (fun j {CAst.v = idl, patl, _} ->
+      CAst.make
+      @@
+      if Int.equal j i then (idl, patl, mkGRef (Lazy.force coq_True_ref))
+      else (idl, patl, mkGRef (Lazy.force coq_False_ref)))
     0
+
 (*
    [make_discr_match brl el i] generates an hypothesis such that it reduce to true iff
    brl_{i} is the first branch matched by [el]
 
    Used when we want to simulate the coq pattern matching algorithm
 *)
-let make_discr_match brl =
-  fun el i ->
-  mkGCases(None,
-           make_discr_match_el el,
-           make_discr_match_brl i brl)
+let make_discr_match brl el i =
+  mkGCases (None, make_discr_match_el el, make_discr_match_brl i brl)
 
 (**********************************************************************)
 (*  functions used to build case expression from lettuple and if ones *)
@@ -307,140 +272,159 @@ let make_discr_match brl =
 
 (* [build_constructors_of_type] construct the array of pattern of its inductive argument*)
 let build_constructors_of_type ind' argl =
-  let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
+  let mib, ind = Inductive.lookup_mind_specif (Global.env ()) ind' in
   let npar = mib.Declarations.mind_nparams in
-  Array.mapi (fun i _ ->
-                let construct = ind',i+1 in
-                let constructref = GlobRef.ConstructRef(construct) in
-                let _implicit_positions_of_cst =
-                  Impargs.implicits_of_global constructref
-                in
-                let cst_narg =
-                  Inductiveops.constructor_nallargs
-                    (Global.env ())
-                    construct
-                in
-                let argl =
-                  if List.is_empty argl then
-                    List.make cst_narg (mkGHole ())
-                  else
-                    List.make npar (mkGHole ()) @ argl
-                in
-                let pat_as_term =
-                  mkGApp(mkGRef (GlobRef.ConstructRef(ind',i+1)),argl)
-                in
-                cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
-             )
+  Array.mapi
+    (fun i _ ->
+      let construct = (ind', i + 1) in
+      let constructref = GlobRef.ConstructRef construct in
+      let _implicit_positions_of_cst =
+        Impargs.implicits_of_global constructref
+      in
+      let cst_narg =
+        Inductiveops.constructor_nallargs (Global.env ()) construct
+      in
+      let argl =
+        if List.is_empty argl then List.make cst_narg (mkGHole ())
+        else List.make npar (mkGHole ()) @ argl
+      in
+      let pat_as_term =
+        mkGApp (mkGRef (GlobRef.ConstructRef (ind', i + 1)), argl)
+      in
+      cases_pattern_of_glob_constr (Global.env ()) Anonymous pat_as_term)
     ind.Declarations.mind_consnames
 
 (******************)
 (* Main functions *)
 (******************)
 
-
-
-let raw_push_named (na,raw_value,raw_typ) env =
+let raw_push_named (na, raw_value, raw_typ) env =
   match na with
-    | Anonymous -> env
-    | Name id ->
-      let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
-      let na = make_annot id Sorts.Relevant in (* TODO relevance *)
-        (match raw_value with
-        | None ->
-           EConstr.push_named (NamedDecl.LocalAssum (na,typ)) env
-        | Some value ->
-           EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env)
-
+  | Anonymous -> env
+  | Name id -> (
+    let typ, _ =
+      Pretyping.understand env (Evd.from_env env)
+        ~expected_type:Pretyping.IsType raw_typ
+    in
+    let na = make_annot id Sorts.Relevant in
+    (* TODO relevance *)
+    match raw_value with
+    | None -> EConstr.push_named (NamedDecl.LocalAssum (na, typ)) env
+    | Some value -> EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env
+    )
 
 let add_pat_variables sigma pat typ env : Environ.env =
-  let rec add_pat_variables env pat typ  : Environ.env =
-    observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
-
+  let rec add_pat_variables env pat typ : Environ.env =
+    observe
+      (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
     match DAst.get pat with
-      | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (make_annot na Sorts.Relevant,typ)) env
-      | PatCstr(c,patl,na) ->
-          let Inductiveops.IndType(indf,indargs) =
-            try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
-            with Not_found -> assert false
-          in
-          let constructors = Inductiveops.get_constructors env indf in
-          let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
-          let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in
-          List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
+    | PatVar na ->
+      Environ.push_rel
+        (RelDecl.LocalAssum (make_annot na Sorts.Relevant, typ))
+        env
+    | PatCstr (c, patl, na) ->
+      let (Inductiveops.IndType (indf, indargs)) =
+        try
+          Inductiveops.find_rectype env (Evd.from_env env)
+            (EConstr.of_constr typ)
+        with Not_found -> assert false
+      in
+      let constructors = Inductiveops.get_constructors env indf in
+      let constructor : Inductiveops.constructor_summary =
+        List.find
+          (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr))
+          (Array.to_list constructors)
+      in
+      let cs_args_types : types list =
+        List.map RelDecl.get_type constructor.Inductiveops.cs_args
+      in
+      List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
   in
   let new_env = add_pat_variables env pat typ in
   let res =
-    fst (
-      Context.Rel.fold_outside
-        (fun decl (env,ctxt) ->
+    fst
+      (Context.Rel.fold_outside
+         (fun decl (env, ctxt) ->
            let open Context.Rel.Declaration in
            match decl with
-           | LocalAssum ({binder_name=Anonymous},_) | LocalDef ({binder_name=Anonymous},_,_) -> assert false
-           | LocalAssum ({binder_name=Name id} as na, t) ->
-             let na = {na with binder_name=id} in
-             let new_t =  substl ctxt t in
-             observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
-                      str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
-                      str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl ()
-                     );
+           | LocalAssum ({binder_name = Anonymous}, _)
+            |LocalDef ({binder_name = Anonymous}, _, _) ->
+             assert false
+           | LocalAssum (({binder_name = Name id} as na), t) ->
+             let na = {na with binder_name = id} in
+             let new_t = substl ctxt t in
+             observe
+               ( str "for variable " ++ Ppconstr.pr_id id ++ fnl ()
+               ++ str "old type := "
+               ++ Printer.pr_lconstr_env env sigma t
+               ++ fnl () ++ str "new type := "
+               ++ Printer.pr_lconstr_env env sigma new_t
+               ++ fnl () );
              let open Context.Named.Declaration in
-             (Environ.push_named (LocalAssum (na,new_t)) env,mkVar id::ctxt)
-           | LocalDef ({binder_name=Name id} as na, v, t) ->
-             let na = {na with binder_name=id} in
-             let new_t =  substl ctxt t in
+             (Environ.push_named (LocalAssum (na, new_t)) env, mkVar id :: ctxt)
+           | LocalDef (({binder_name = Name id} as na), v, t) ->
+             let na = {na with binder_name = id} in
+             let new_t = substl ctxt t in
              let new_v = substl ctxt v in
-             observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
-                      str "old type := "  ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
-                      str "new type := "  ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++
-                      str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++
-                      str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl ()
-                     );
+             observe
+               ( str "for variable " ++ Ppconstr.pr_id id ++ fnl ()
+               ++ str "old type := "
+               ++ Printer.pr_lconstr_env env sigma t
+               ++ fnl () ++ str "new type := "
+               ++ Printer.pr_lconstr_env env sigma new_t
+               ++ fnl () ++ str "old value := "
+               ++ Printer.pr_lconstr_env env sigma v
+               ++ fnl () ++ str "new value := "
+               ++ Printer.pr_lconstr_env env sigma new_v
+               ++ fnl () );
              let open Context.Named.Declaration in
-             (Environ.push_named (LocalDef (na,new_v,new_t)) env,mkVar id::ctxt)
-        )
-        (Environ.rel_context new_env)
-        ~init:(env,[])
-    )
+             ( Environ.push_named (LocalDef (na, new_v, new_t)) env
+             , mkVar id :: ctxt ))
+         (Environ.rel_context new_env)
+         ~init:(env, []))
   in
-  observe (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
+  observe
+    (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
   res
 
-
-
-
-let rec pattern_to_term_and_type env typ  = DAst.with_val (function
-  | PatVar Anonymous -> assert false
-  | PatVar (Name id) ->
-        mkGVar id
-  | PatCstr(constr,patternl,_) ->
-      let cst_narg =
-        Inductiveops.constructor_nallargs
-          (Global.env ())
-          constr
-      in
-      let Inductiveops.IndType(indf,indargs) =
-        try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
+let rec pattern_to_term_and_type env typ =
+  DAst.with_val (function
+    | PatVar Anonymous -> assert false
+    | PatVar (Name id) -> mkGVar id
+    | PatCstr (constr, patternl, _) ->
+      let cst_narg = Inductiveops.constructor_nallargs (Global.env ()) constr in
+      let (Inductiveops.IndType (indf, indargs)) =
+        try
+          Inductiveops.find_rectype env (Evd.from_env env)
+            (EConstr.of_constr typ)
         with Not_found -> assert false
       in
       let constructors = Inductiveops.get_constructors env indf in
-      let constructor  = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
-      let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in
-      let _,cstl = Inductiveops.dest_ind_family indf in
+      let constructor =
+        List.find
+          (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr)
+          (Array.to_list constructors)
+      in
+      let cs_args_types : types list =
+        List.map RelDecl.get_type constructor.Inductiveops.cs_args
+      in
+      let _, cstl = Inductiveops.dest_ind_family indf in
       let csta = Array.of_list cstl in
       let implicit_args =
         Array.to_list
           (Array.init
              (cst_narg - List.length patternl)
-             (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i)))
-          )
+             (fun i ->
+               Detyping.detype Detyping.Now false Id.Set.empty env
+                 (Evd.from_env env)
+                 (EConstr.of_constr csta.(i))))
       in
       let patl_as_term =
-        List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
+        List.map2
+          (pattern_to_term_and_type env)
+          (List.rev cs_args_types) patternl
       in
-      mkGApp(mkGRef(GlobRef.ConstructRef constr),
-             implicit_args@patl_as_term
-            )
-  )
+      mkGApp (mkGRef (GlobRef.ConstructRef constr), implicit_args @ patl_as_term))
 
 (* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return)
    of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the
@@ -473,448 +457,427 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
    but only the value of the function
 *)
 
-
-let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_return =
+let rec build_entry_lc env sigma funnames avoid rt :
+    glob_constr build_entry_return =
   observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
   let open CAst in
   match DAst.get rt with
-    | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ | GInt _ | GFloat _ ->
-        (* do nothing (except changing type of course) *)
-        mk_result [] rt avoid
-    | GApp(_,_) ->
-        let f,args = glob_decompose_app rt in
-        let args_res : (glob_constr list) build_entry_return =
-          List.fold_right (* create the arguments lists of constructors and combine them *)
-            (fun arg ctxt_argsl ->
-               let arg_res = build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg in
-               combine_results combine_args arg_res ctxt_argsl
-            )
-            args
-            (mk_result [] [] avoid)
-        in
-        begin
-          match DAst.get f with
-            | GLambda _  ->
-                let rec aux t l =
-                  match l with
-                    | [] -> t
-                    | u::l -> DAst.make @@
-                        match DAst.get t with
-                          | GLambda(na,_,nat,b) ->
-                              GLetIn(na,u,None,aux b l)
-                          | _ ->
-                              GApp(t,l)
-                in
-                build_entry_lc env sigma funnames avoid (aux f args)
-            | GVar id when Id.Set.mem id funnames ->
-                (* if we have [f t1 ... tn] with [f]$\in$[fnames]
-                   then we create a fresh variable [res],
-                   add [res] and its "value" (i.e. [res v1 ... vn]) to each
-                   pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and
-                   a pseudo value "v1 ... vn".
-                   The "value" of this branch is then simply [res]
-                *)
-                (* XXX here and other [understand] calls drop the ctx *)
-                let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
-                let rt_typ = Retyping.get_type_of env (Evd.from_env env) rt_as_constr in
-                let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
-                let res = fresh_id args_res.to_avoid "_res" in
-                let new_avoid = res::args_res.to_avoid in
-                let res_rt = mkGVar res in
-                let new_result =
-                  List.map
-                    (fun arg_res ->
-                       let new_hyps =
-                         [Prod (Name res),res_raw_type;
-                          Prod Anonymous,mkGApp(res_rt,(mkGVar id)::arg_res.value)]
-                       in
-                       {context =  arg_res.context@new_hyps; value = res_rt }
-                    )
-                    args_res.result
-                in
-                { result = new_result; to_avoid = new_avoid }
-            | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ ->
-                (* if have [g t1 ... tn] with [g] not appearing in [funnames]
-                   then
-                   foreach [ctxt,v1 ... vn] in [args_res] we return
-                   [ctxt, g v1 .... vn]
-                *)
-                {
-                  args_res with
-                    result =
-                    List.map
-                      (fun args_res ->
-                         {args_res with value = mkGApp(f,args_res.value)})
-                      args_res.result
-                }
-            | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
-            | GLetIn(n,v,t,b) ->
-                (* if we have [(let x := v in b) t1 ... tn] ,
-                   we discard our work and compute the list of constructor for
-                   [let x = v in (b t1 ... tn)] up to alpha conversion
-                *)
-                let new_n,new_b,new_avoid =
-                  match n with
-                    | Name id when List.exists (is_free_in id) args ->
-                        (* need to alpha-convert the name *)
-                        let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in
-                        let new_avoid = id:: avoid in
-                        let new_b =
-                          replace_var_by_term
-                            id
-                            (DAst.make @@ GVar id)
-                            b
-                        in
-                        (Name new_id,new_b,new_avoid)
-                    | _ -> n,b,avoid
-                in
-                build_entry_lc
-                  env
-      sigma
-      funnames
-                  avoid
-                  (mkGLetIn(new_n,v,t,mkGApp(new_b,args)))
-            | GCases _  | GIf _ | GLetTuple _ ->
-                (* we have [(match e1, ...., en with ..... end) t1 tn]
-                   we first compute the result from the case and
-                   then combine each of them with each of args one
-                *)
-                let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in
-                combine_results combine_app f_res  args_res
-            | GCast(b,_) ->
-                (* for an applied cast we just trash the cast part
-                   and restart the work.
-
-                   WARNING: We need to restart since [b] itself should be an application term
-                *)
-                build_entry_lc env sigma funnames avoid (mkGApp(b,args))
-            | GRec _ -> user_err Pp.(str "Not handled GRec")
-            | GProd _ -> user_err Pp.(str "Cannot apply a type")
-            | GInt _ -> user_err Pp.(str "Cannot apply an integer")
-      | GFloat _ -> user_err Pp.(str "Cannot apply a float")
-        end (* end of the application treatement *)
-
-    | GLambda(n,_,t,b) ->
-        (* we first compute the list of constructor
-           corresponding to the body of the function,
-           then the one corresponding to the type
-           and combine the two result
-        *)
-        let t_res = build_entry_lc env sigma funnames avoid t  in
-        let new_n =
-          match n with
-            | Name _ -> n
-            | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
-        in
-        let new_env = raw_push_named (new_n,None,t) env in
-        let b_res = build_entry_lc new_env sigma funnames avoid b in
-        combine_results (combine_lam new_n) t_res b_res
-    | GProd(n,_,t,b) ->
-        (* we first compute the list of constructor
-           corresponding to the body of the function,
-           then the one corresponding to the type
-           and combine the two result
-        *)
-        let t_res = build_entry_lc env sigma funnames avoid t in
-        let new_env = raw_push_named (n,None,t) env in
-        let b_res = build_entry_lc new_env sigma funnames avoid b in
-        if List.length t_res.result = 1 && List.length b_res.result = 1
-        then combine_results (combine_prod2 n) t_res b_res
-        else combine_results (combine_prod n) t_res b_res
-    | GLetIn(n,v,typ,b) ->
-        (* we first compute the list of constructor
-           corresponding to the body of the function,
-           then the one corresponding to the value [t]
-           and combine the two result
-        *)
-        let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
-        let v_res = build_entry_lc env sigma funnames avoid v in
-        let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
-        let v_type = Retyping.get_type_of env (Evd.from_env env) v_as_constr in
-        let v_r = Sorts.Relevant in (* TODO relevance *)
-        let new_env =
-          match n with
-              Anonymous -> env
-            | Name id -> EConstr.push_named (NamedDecl.LocalDef (make_annot id v_r,v_as_constr,v_type)) env
-        in
-        let b_res = build_entry_lc new_env sigma funnames avoid b in
-        combine_results (combine_letin n) v_res b_res
-    | GCases(_,_,el,brl) ->
-        (* we create the discrimination function
-           and treat the case itself
-        *)
-        let make_discr = make_discr_match brl in
-        build_entry_lc_from_case env sigma funnames make_discr el brl avoid
-    | GIf(b,(na,e_option),lhs,rhs) ->
-        let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-        let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
-        let (ind,_) =
-          try Inductiveops.find_inductive env (Evd.from_env env) b_typ
-          with Not_found ->
-            user_err  (str "Cannot find the inductive associated to " ++
-                               Printer.pr_glob_constr_env env b ++ str " in " ++
-                               Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
-        in
-        let case_pats = build_constructors_of_type (fst ind) [] in
-        assert (Int.equal (Array.length case_pats) 2);
-        let brl =
-          List.map_i
-            (fun i x -> CAst.make ([],[case_pats.(i)],x))
-            0
-            [lhs;rhs]
-        in
-        let match_expr =
-          mkGCases(None,[(b,(Anonymous,None))],brl)
-        in
-        (* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
-        build_entry_lc env sigma funnames avoid match_expr
-    | GLetTuple(nal,_,b,e) ->
-        begin
-          let nal_as_glob_constr =
-            List.map
-              (function
-                   Name id -> mkGVar id
-                 | Anonymous -> mkGHole ()
-              )
-              nal
-          in
-          let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-          let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
-          let (ind,_) =
-            try Inductiveops.find_inductive env (Evd.from_env env) b_typ
-            with Not_found ->
-              user_err  (str "Cannot find the inductive associated to " ++
-                                 Printer.pr_glob_constr_env env b ++ str " in " ++
-                                 Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
+  | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _
+   |GFloat _ ->
+    (* do nothing (except changing type of course) *)
+    mk_result [] rt avoid
+  | GApp (_, _) -> (
+    let f, args = glob_decompose_app rt in
+    let args_res : glob_constr list build_entry_return =
+      List.fold_right
+        (* create the arguments lists of constructors and combine them *)
+          (fun arg ctxt_argsl ->
+          let arg_res =
+            build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg
           in
-          let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
-          assert (Int.equal (Array.length case_pats) 1);
-          let br = CAst.make ([],[case_pats.(0)],e) in
-          let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
-          build_entry_lc env sigma funnames avoid match_expr
-
-        end
+          combine_results combine_args arg_res ctxt_argsl)
+        args (mk_result [] [] avoid)
+    in
+    match DAst.get f with
+    | GLambda _ ->
+      let rec aux t l =
+        match l with
+        | [] -> t
+        | u :: l -> (
+          DAst.make
+          @@
+          match DAst.get t with
+          | GLambda (na, _, nat, b) -> GLetIn (na, u, None, aux b l)
+          | _ -> GApp (t, l) )
+      in
+      build_entry_lc env sigma funnames avoid (aux f args)
+    | GVar id when Id.Set.mem id funnames ->
+      (* if we have [f t1 ... tn] with [f]$\in$[fnames]
+         then we create a fresh variable [res],
+         add [res] and its "value" (i.e. [res v1 ... vn]) to each
+         pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and
+         a pseudo value "v1 ... vn".
+         The "value" of this branch is then simply [res]
+      *)
+      (* XXX here and other [understand] calls drop the ctx *)
+      let rt_as_constr, ctx = Pretyping.understand env (Evd.from_env env) rt in
+      let rt_typ = Retyping.get_type_of env (Evd.from_env env) rt_as_constr in
+      let res_raw_type =
+        Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env)
+          rt_typ
+      in
+      let res = fresh_id args_res.to_avoid "_res" in
+      let new_avoid = res :: args_res.to_avoid in
+      let res_rt = mkGVar res in
+      let new_result =
+        List.map
+          (fun arg_res ->
+            let new_hyps =
+              [ (Prod (Name res), res_raw_type)
+              ; (Prod Anonymous, mkGApp (res_rt, mkGVar id :: arg_res.value)) ]
+            in
+            {context = arg_res.context @ new_hyps; value = res_rt})
+          args_res.result
+      in
+      {result = new_result; to_avoid = new_avoid}
+    | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ ->
+      (* if have [g t1 ... tn] with [g] not appearing in [funnames]
+         then
+         foreach [ctxt,v1 ... vn] in [args_res] we return
+         [ctxt, g v1 .... vn]
+      *)
+      { args_res with
+        result =
+          List.map
+            (fun args_res -> {args_res with value = mkGApp (f, args_res.value)})
+            args_res.result }
+    | GApp _ ->
+      assert false (* we have collected all the app in [glob_decompose_app] *)
+    | GLetIn (n, v, t, b) ->
+      (* if we have [(let x := v in b) t1 ... tn] ,
+         we discard our work and compute the list of constructor for
+         [let x = v in (b t1 ... tn)] up to alpha conversion
+      *)
+      let new_n, new_b, new_avoid =
+        match n with
+        | Name id when List.exists (is_free_in id) args ->
+          (* need to alpha-convert the name *)
+          let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in
+          let new_avoid = id :: avoid in
+          let new_b = replace_var_by_term id (DAst.make @@ GVar id) b in
+          (Name new_id, new_b, new_avoid)
+        | _ -> (n, b, avoid)
+      in
+      build_entry_lc env sigma funnames avoid
+        (mkGLetIn (new_n, v, t, mkGApp (new_b, args)))
+    | GCases _ | GIf _ | GLetTuple _ ->
+      (* we have [(match e1, ...., en with ..... end) t1 tn]
+         we first compute the result from the case and
+         then combine each of them with each of args one
+      *)
+      let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in
+      combine_results combine_app f_res args_res
+    | GCast (b, _) ->
+      (* for an applied cast we just trash the cast part
+         and restart the work.
+
+         WARNING: We need to restart since [b] itself should be an application term
+      *)
+      build_entry_lc env sigma funnames avoid (mkGApp (b, args))
     | GRec _ -> user_err Pp.(str "Not handled GRec")
-    | GCast(b,_) ->
-        build_entry_lc env sigma funnames  avoid b
-and build_entry_lc_from_case env sigma funname make_discr
-    (el:tomatch_tuples)
-    (brl:Glob_term.cases_clauses) avoid :
-    glob_constr build_entry_return =
+    | GProd _ -> user_err Pp.(str "Cannot apply a type")
+    | GInt _ -> user_err Pp.(str "Cannot apply an integer")
+    | GFloat _ -> user_err Pp.(str "Cannot apply a float")
+    (* end of the application treatement *) )
+  | GLambda (n, _, t, b) ->
+    (* we first compute the list of constructor
+       corresponding to the body of the function,
+       then the one corresponding to the type
+       and combine the two result
+    *)
+    let t_res = build_entry_lc env sigma funnames avoid t in
+    let new_n =
+      match n with
+      | Name _ -> n
+      | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
+    in
+    let new_env = raw_push_named (new_n, None, t) env in
+    let b_res = build_entry_lc new_env sigma funnames avoid b in
+    combine_results (combine_lam new_n) t_res b_res
+  | GProd (n, _, t, b) ->
+    (* we first compute the list of constructor
+       corresponding to the body of the function,
+       then the one corresponding to the type
+       and combine the two result
+    *)
+    let t_res = build_entry_lc env sigma funnames avoid t in
+    let new_env = raw_push_named (n, None, t) env in
+    let b_res = build_entry_lc new_env sigma funnames avoid b in
+    if List.length t_res.result = 1 && List.length b_res.result = 1 then
+      combine_results (combine_prod2 n) t_res b_res
+    else combine_results (combine_prod n) t_res b_res
+  | GLetIn (n, v, typ, b) ->
+    (* we first compute the list of constructor
+       corresponding to the body of the function,
+       then the one corresponding to the value [t]
+       and combine the two result
+    *)
+    let v =
+      match typ with
+      | None -> v
+      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, CastConv t)
+    in
+    let v_res = build_entry_lc env sigma funnames avoid v in
+    let v_as_constr, ctx = Pretyping.understand env (Evd.from_env env) v in
+    let v_type = Retyping.get_type_of env (Evd.from_env env) v_as_constr in
+    let v_r = Sorts.Relevant in
+    (* TODO relevance *)
+    let new_env =
+      match n with
+      | Anonymous -> env
+      | Name id ->
+        EConstr.push_named
+          (NamedDecl.LocalDef (make_annot id v_r, v_as_constr, v_type))
+          env
+    in
+    let b_res = build_entry_lc new_env sigma funnames avoid b in
+    combine_results (combine_letin n) v_res b_res
+  | GCases (_, _, el, brl) ->
+    (* we create the discrimination function
+       and treat the case itself
+    *)
+    let make_discr = make_discr_match brl in
+    build_entry_lc_from_case env sigma funnames make_discr el brl avoid
+  | GIf (b, (na, e_option), lhs, rhs) ->
+    let b_as_constr, ctx = Pretyping.understand env (Evd.from_env env) b in
+    let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
+    let ind, _ =
+      try Inductiveops.find_inductive env (Evd.from_env env) b_typ
+      with Not_found ->
+        user_err
+          ( str "Cannot find the inductive associated to "
+          ++ Printer.pr_glob_constr_env env b
+          ++ str " in "
+          ++ Printer.pr_glob_constr_env env rt
+          ++ str ". try again with a cast" )
+    in
+    let case_pats = build_constructors_of_type (fst ind) [] in
+    assert (Int.equal (Array.length case_pats) 2);
+    let brl =
+      List.map_i (fun i x -> CAst.make ([], [case_pats.(i)], x)) 0 [lhs; rhs]
+    in
+    let match_expr = mkGCases (None, [(b, (Anonymous, None))], brl) in
+    (* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
+    build_entry_lc env sigma funnames avoid match_expr
+  | GLetTuple (nal, _, b, e) ->
+    let nal_as_glob_constr =
+      List.map (function Name id -> mkGVar id | Anonymous -> mkGHole ()) nal
+    in
+    let b_as_constr, ctx = Pretyping.understand env (Evd.from_env env) b in
+    let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
+    let ind, _ =
+      try Inductiveops.find_inductive env (Evd.from_env env) b_typ
+      with Not_found ->
+        user_err
+          ( str "Cannot find the inductive associated to "
+          ++ Printer.pr_glob_constr_env env b
+          ++ str " in "
+          ++ Printer.pr_glob_constr_env env rt
+          ++ str ". try again with a cast" )
+    in
+    let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
+    assert (Int.equal (Array.length case_pats) 1);
+    let br = CAst.make ([], [case_pats.(0)], e) in
+    let match_expr = mkGCases (None, [(b, (Anonymous, None))], [br]) in
+    build_entry_lc env sigma funnames avoid match_expr
+  | GRec _ -> user_err Pp.(str "Not handled GRec")
+  | GCast (b, _) -> build_entry_lc env sigma funnames avoid b
+
+and build_entry_lc_from_case env sigma funname make_discr (el : tomatch_tuples)
+    (brl : Glob_term.cases_clauses) avoid : glob_constr build_entry_return =
   match el with
-    | [] -> assert false (* this case correspond to match <nothing> with .... !*)
-    | el ->
-        (* this case correspond to
-           match el with brl end
-           we first compute the list of lists corresponding to [el] and
-           combine them .
-           Then for each element of the combinations,
-           we compute the result we compute one list per branch in [brl] and
-           finally we just concatenate those list
-        *)
-        let case_resl =
-            List.fold_right
-              (fun (case_arg,_) ctxt_argsl ->
-                let arg_res = build_entry_lc env sigma funname ctxt_argsl.to_avoid case_arg in
-                combine_results combine_args arg_res ctxt_argsl
-              )
-              el
-              (mk_result [] [] avoid)
-        in
-        let types =
-          List.map (fun (case_arg,_) ->
-                      let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
-                      EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) case_arg_as_constr)
-                   ) el
-        in
-        (****** The next works only if the match is not dependent ****)
-        let results =
-          List.map
-            (fun ca ->
-               let res = build_entry_lc_from_case_term
-               env sigma types
-               funname (make_discr)
-               []  brl
-               case_resl.to_avoid
-               ca
-               in
-               res
-            )
-            case_resl.result
-        in
-        {
-          result = List.concat (List.map (fun r -> r.result) results);
-          to_avoid =
-            List.fold_left (fun acc r -> List.union Id.equal acc r.to_avoid)
-              [] results
-        }
-
-and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to_prevent brl avoid
-    matched_expr =
+  | [] -> assert false (* this case correspond to match <nothing> with .... !*)
+  | el ->
+    (* this case correspond to
+       match el with brl end
+       we first compute the list of lists corresponding to [el] and
+       combine them .
+       Then for each element of the combinations,
+       we compute the result we compute one list per branch in [brl] and
+       finally we just concatenate those list
+    *)
+    let case_resl =
+      List.fold_right
+        (fun (case_arg, _) ctxt_argsl ->
+          let arg_res =
+            build_entry_lc env sigma funname ctxt_argsl.to_avoid case_arg
+          in
+          combine_results combine_args arg_res ctxt_argsl)
+        el (mk_result [] [] avoid)
+    in
+    let types =
+      List.map
+        (fun (case_arg, _) ->
+          let case_arg_as_constr, ctx =
+            Pretyping.understand env (Evd.from_env env) case_arg
+          in
+          EConstr.Unsafe.to_constr
+            (Retyping.get_type_of env (Evd.from_env env) case_arg_as_constr))
+        el
+    in
+    (****** The next works only if the match is not dependent ****)
+    let results =
+      List.map
+        (fun ca ->
+          let res =
+            build_entry_lc_from_case_term env sigma types funname make_discr []
+              brl case_resl.to_avoid ca
+          in
+          res)
+        case_resl.result
+    in
+    { result = List.concat (List.map (fun r -> r.result) results)
+    ; to_avoid =
+        List.fold_left
+          (fun acc r -> List.union Id.equal acc r.to_avoid)
+          [] results }
+
+and build_entry_lc_from_case_term env sigma types funname make_discr
+    patterns_to_prevent brl avoid matched_expr =
   match brl with
-    | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
-    | br::brl' ->
-        (* alpha conversion to prevent name clashes *)
-        let {CAst.v=(idl,patl,return)} = alpha_br avoid br in
-        let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
-        (* building a list of precondition stating that we are not in this branch
-           (will be used in the following recursive calls)
-        *)
-        let new_env = List.fold_right2 (add_pat_variables sigma) patl types env in
-        let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
-          List.map2
-            (fun pat typ ->
-               fun avoid pat'_as_term ->
-                 let renamed_pat,_,_ = alpha_pat avoid pat in
-                 let pat_ids = get_pattern_id renamed_pat  in
-                 let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
-                   List.fold_right
-                     (fun id acc ->
-                        let typ_of_id = Typing.type_of_variable env_with_pat_ids id in
-                        let raw_typ_of_id =
-                          Detyping.detype Detyping.Now false Id.Set.empty
-                            env_with_pat_ids (Evd.from_env env) typ_of_id
-                        in
-                        mkGProd (Name id,raw_typ_of_id,acc))
-                     pat_ids
-                     (glob_make_neq pat'_as_term (pattern_to_term renamed_pat))
-            )
-            patl
-            types
-        in
-        (* Checking if we can be in this branch
-           (will be used in the following recursive calls)
-        *)
-        let unify_with_those_patterns : (cases_pattern -> bool*bool) list =
-          List.map
-            (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat')
-            patl
-        in
-        (*
+  | [] -> (* computed_branches  *) {result = []; to_avoid = avoid}
+  | br :: brl' ->
+    (* alpha conversion to prevent name clashes *)
+    let {CAst.v = idl, patl, return} = alpha_br avoid br in
+    let new_avoid = idl @ avoid in
+    (* for now we can no more use idl as an identifier *)
+    (* building a list of precondition stating that we are not in this branch
+       (will be used in the following recursive calls)
+    *)
+    let new_env = List.fold_right2 (add_pat_variables sigma) patl types env in
+    let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
+      List.map2
+        (fun pat typ avoid pat'_as_term ->
+          let renamed_pat, _, _ = alpha_pat avoid pat in
+          let pat_ids = get_pattern_id renamed_pat in
+          let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
+          List.fold_right
+            (fun id acc ->
+              let typ_of_id = Typing.type_of_variable env_with_pat_ids id in
+              let raw_typ_of_id =
+                Detyping.detype Detyping.Now false Id.Set.empty env_with_pat_ids
+                  (Evd.from_env env) typ_of_id
+              in
+              mkGProd (Name id, raw_typ_of_id, acc))
+            pat_ids
+            (glob_make_neq pat'_as_term (pattern_to_term renamed_pat)))
+        patl types
+    in
+    (* Checking if we can be in this branch
+       (will be used in the following recursive calls)
+    *)
+    let unify_with_those_patterns : (cases_pattern -> bool * bool) list =
+      List.map
+        (fun pat pat' -> (are_unifiable pat pat', eq_cases_pattern pat pat'))
+        patl
+    in
+    (*
            we first compute the other branch result (in ordrer to keep the order of the matching
            as much as possible)
         *)
-        let brl'_res =
-          build_entry_lc_from_case_term
-            env
-      sigma
-            types
-            funname
-            make_discr
-            ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
-            brl'
-            avoid
-            matched_expr
-        in
-        (* We now create the precondition of this branch i.e.
-           1- the list of variable appearing in the different patterns of this branch and
-              the list of equation stating than el = patl (List.flatten ...)
-           2- If there exists a previous branch which pattern unify with the one of this branch
-              then a discrimination precond stating that we are not in a previous branch (if List.exists ...)
-        *)
-        let those_pattern_preconds =
-          (List.flatten
-            (
-              List.map3
-              (fun pat e typ_as_constr ->
-                 let this_pat_ids = ids_of_pat pat in
-                 let typ_as_constr = EConstr.of_constr typ_as_constr in
-                 let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in
-                 let pat_as_term = pattern_to_term pat in
-                 (* removing trivial holes *)
-                 let pat_as_term = solve_trivial_holes pat_as_term e in
-                  (* observe (str "those_pattern_preconds" ++ spc () ++ *)
-                  (*            str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *)
-                  (*            str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *)
-                  (*            str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *)
-                 List.fold_right
-                   (fun id  acc ->
-                      if Id.Set.mem id this_pat_ids
-                      then (Prod (Name id),
-                      let typ_of_id = Typing.type_of_variable new_env id in
-                      let raw_typ_of_id =
-                        Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
-                      in
-                      raw_typ_of_id
-                           )::acc
-                      else acc
-                   )
-                   idl
-                   [(Prod Anonymous,glob_make_eq ~typ pat_as_term e)]
-              )
-              patl
-              matched_expr.value
-              types
-          )
-          )
-          @
-          (if List.exists (function (unifl,_) ->
-                             let (unif,_) =
-                               List.split (List.map2 (fun x y -> x y) unifl patl)
-                             in
-                             List.for_all (fun x -> x) unif) patterns_to_prevent
-           then
-             let i = List.length patterns_to_prevent in
-             let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in
-             [(Prod Anonymous,make_discr pats_as_constr i  )]
-           else
-             []
-          )
-        in
-        (* We compute the result of the value returned by the branch*)
-        let return_res = build_entry_lc new_env sigma funname new_avoid return in
-        (* and combine it with the preconds computed for this branch *)
-        let this_branch_res =
-          List.map
-            (fun res  ->
-               { context = matched_expr.context@those_pattern_preconds@res.context ;
-                 value = res.value}
-            )
-            return_res.result
+    let brl'_res =
+      build_entry_lc_from_case_term env sigma types funname make_discr
+        ((unify_with_those_patterns, not_those_patterns) :: patterns_to_prevent)
+        brl' avoid matched_expr
+    in
+    (* We now create the precondition of this branch i.e.
+       1- the list of variable appearing in the different patterns of this branch and
+          the list of equation stating than el = patl (List.flatten ...)
+       2- If there exists a previous branch which pattern unify with the one of this branch
+          then a discrimination precond stating that we are not in a previous branch (if List.exists ...)
+    *)
+    let those_pattern_preconds =
+      List.flatten
+        (List.map3
+           (fun pat e typ_as_constr ->
+             let this_pat_ids = ids_of_pat pat in
+             let typ_as_constr = EConstr.of_constr typ_as_constr in
+             let typ =
+               Detyping.detype Detyping.Now false Id.Set.empty new_env
+                 (Evd.from_env env) typ_as_constr
+             in
+             let pat_as_term = pattern_to_term pat in
+             (* removing trivial holes *)
+             let pat_as_term = solve_trivial_holes pat_as_term e in
+             (* observe (str "those_pattern_preconds" ++ spc () ++ *)
+             (*            str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *)
+             (*            str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *)
+             (*            str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *)
+             List.fold_right
+               (fun id acc ->
+                 if Id.Set.mem id this_pat_ids then
+                   ( Prod (Name id)
+                   , let typ_of_id = Typing.type_of_variable new_env id in
+                     let raw_typ_of_id =
+                       Detyping.detype Detyping.Now false Id.Set.empty new_env
+                         (Evd.from_env env) typ_of_id
+                     in
+                     raw_typ_of_id )
+                   :: acc
+                 else acc)
+               idl
+               [(Prod Anonymous, glob_make_eq ~typ pat_as_term e)])
+           patl matched_expr.value types)
+      @
+      if
+        List.exists
+          (function
+            | unifl, _ ->
+              let unif, _ =
+                List.split (List.map2 (fun x y -> x y) unifl patl)
+              in
+              List.for_all (fun x -> x) unif)
+          patterns_to_prevent
+      then
+        let i = List.length patterns_to_prevent in
+        let pats_as_constr =
+          List.map2 (pattern_to_term_and_type new_env) types patl
         in
-        { brl'_res with result = this_branch_res@brl'_res.result }
-
+        [(Prod Anonymous, make_discr pats_as_constr i)]
+      else []
+    in
+    (* We compute the result of the value returned by the branch*)
+    let return_res = build_entry_lc new_env sigma funname new_avoid return in
+    (* and combine it with the preconds computed for this branch *)
+    let this_branch_res =
+      List.map
+        (fun res ->
+          { context = matched_expr.context @ those_pattern_preconds @ res.context
+          ; value = res.value })
+        return_res.result
+    in
+    {brl'_res with result = this_branch_res @ brl'_res.result}
 
-let is_res r = match DAst.get r with
-| GVar id ->
-  begin try
-    String.equal (String.sub (Id.to_string id) 0 4) "_res"
-  with Invalid_argument _ -> false end
-| _ -> false
+let is_res r =
+  match DAst.get r with
+  | GVar id -> (
+    try String.equal (String.sub (Id.to_string id) 0 4) "_res"
+    with Invalid_argument _ -> false )
+  | _ -> false
 
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
+let is_gr c gr =
+  match DAst.get c with GRef (r, _) -> GlobRef.equal r gr | _ -> false
 
-let is_gvar c = match DAst.get c with
-| GVar id -> true
-| _ -> false
+let is_gvar c = match DAst.get c with GVar id -> true | _ -> false
 
 let same_raw_term rt1 rt2 =
-  match DAst.get rt1, DAst.get rt2 with
-    | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2
-    | GHole _, GHole _ -> true
-    | _ -> false
+  match (DAst.get rt1, DAst.get rt2) with
+  | GRef (r1, _), GRef (r2, _) -> GlobRef.equal r1 r2
+  | GHole _, GHole _ -> true
+  | _ -> false
+
 let decompose_raw_eq env lhs rhs =
   let rec decompose_raw_eq lhs rhs acc =
-    observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs);
-    let (rhd,lrhs) = glob_decompose_app rhs in
-    let (lhd,llhs) = glob_decompose_app lhs in
+    observe
+      ( str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " "
+      ++ pr_glob_constr_env env rhs );
+    let rhd, lrhs = glob_decompose_app rhs in
+    let lhd, llhs = glob_decompose_app lhs in
     observe (str "lhd := " ++ pr_glob_constr_env env lhd);
     observe (str "rhd := " ++ pr_glob_constr_env env rhd);
     observe (str "llhs := " ++ int (List.length llhs));
     observe (str "lrhs := " ++ int (List.length lrhs));
     let sllhs = List.length llhs in
     let slrhs = List.length lrhs in
-    if same_raw_term lhd rhd && Int.equal sllhs slrhs
-    then
+    if same_raw_term lhd rhd && Int.equal sllhs slrhs then
       (* let _ = assert false in  *)
-      List.fold_right2 decompose_raw_eq	llhs lrhs acc
-    else (lhs,rhs)::acc
+      List.fold_right2 decompose_raw_eq llhs lrhs acc
+    else (lhs, rhs) :: acc
   in
   decompose_raw_eq lhs rhs []
 
 exception Continue
+
 (*
    The second phase which reconstruct the real type of the constructor.
    rebuild the globalized constructors expression.
@@ -925,304 +888,283 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
   let open Context.Rel.Declaration in
   let open CAst in
   match DAst.get rt with
-    | GProd(n,k,t,b) ->
-        let not_free_in_t id = not (is_free_in id t) in
-        let new_crossed_types = t::crossed_types in
-        begin
-          match DAst.get t with
-            | GApp(res_rt ,args') when is_res res_rt ->
-                begin
-                  let arg = List.hd args' in
-                  match DAst.get arg with
-                    | GVar this_relname ->
-                        (*i The next call to mk_rel_id is
-                          valid since we are constructing the graph
-                          Ensures by: obvious
-                          i*)
-
-                        let new_t =
-                          mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
-                        in
-                        let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
-                        let r = Sorts.Relevant in (* TODO relevance *)
-                        let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
-                        let new_b,id_to_exclude =
-                          rebuild_cons new_env
-                            nb_args relname
-                            args new_crossed_types
-                            (depth + 1) b
-                        in
-                        mkGProd(n,new_t,new_b),
-                        Id.Set.filter not_free_in_t id_to_exclude
-                    | _ -> (* the first args is the name of the function! *)
-                        assert false
-                end
-            | GApp(eq_as_ref,[ty; id ;rt])
-                when is_gvar id && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type")  && n == Anonymous
-                  ->
-                let loc1 = rt.CAst.loc in
-                let loc2 = eq_as_ref.CAst.loc in
-                let loc3 = id.CAst.loc in
-                let id = match DAst.get id with GVar id -> id | _ -> assert false in
-                begin
-                  try
-                    observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt);
-                    let t' =
-                      try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
-                      with e when CErrors.noncritical e -> raise Continue
-                    in
-                    let is_in_b = is_free_in id b in
-                    let _keep_eq =
-                      not (List.exists (is_free_in id) args) || is_in_b  ||
-                        List.exists (is_free_in id) crossed_types
-                    in
-                    let new_args = List.map (replace_var_by_term id rt) args in
-                    let subst_b =
-                      if is_in_b then b else  replace_var_by_term id rt b
-                    in
-                    let r = Sorts.Relevant in (* TODO relevance *)
-                    let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
-                    let new_b,id_to_exclude =
-                      rebuild_cons
-                        new_env
-                        nb_args relname
-                        new_args new_crossed_types
-                        (depth + 1) subst_b
-                    in
-                    mkGProd(n,t,new_b),id_to_exclude
-                  with Continue ->
-                    let jmeq = GlobRef.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
-                    let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
-                    let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in
-                    let mib,_ = Global.lookup_inductive (fst ind) in
-                    let nparam = mib.Declarations.mind_nparams in
-                    let params,arg' =
-                      ((Util.List.chop nparam args'))
-                    in
-                    let rt_typ = DAst.make @@
-                       GApp(DAst.make @@ GRef (GlobRef.IndRef (fst ind),None),
-                            (List.map
-                              (fun p -> Detyping.detype Detyping.Now false Id.Set.empty
-                                 env (Evd.from_env env)
-                                 (EConstr.of_constr p)) params)@(Array.to_list
-                                      (Array.make
-                                         (List.length args' - nparam)
-                                         (mkGHole ()))))
-                    in
-                    let eq' =
-                      DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
-                    in
-                    observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
-                    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
-                    observe (str " computing new type for jmeq : done") ;
-                    let sigma = Evd.(from_env env) in
-                    let new_args =
-                      match EConstr.kind sigma eq'_as_constr with
-                        | App(_,[|_;_;ty;_|]) ->
-                            let ty = Array.to_list (snd (EConstr.destApp sigma ty)) in
-                            let ty' = snd (Util.List.chop nparam ty) in
-                            List.fold_left2
-                              (fun acc var_as_constr arg ->
-                                 if isRel var_as_constr
-                                 then
-                                   let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
-                                   match na with
-                                     | Anonymous -> acc
-                                     | Name id' ->
-                                         (id',Detyping.detype Detyping.Now false Id.Set.empty
-                                            env
-                                            (Evd.from_env env)
-                                            arg)::acc
-                                 else if isVar var_as_constr
-                                 then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty
-                                         env
-                                         (Evd.from_env env)
-                                         arg)::acc
-                                 else acc
-                              )
-                              []
-                              arg'
-                              ty'
-                        | _ -> assert false
-                    in
-                    let is_in_b = is_free_in id b in
-                    let _keep_eq =
-                      not (List.exists (is_free_in id) args) || is_in_b  ||
-                        List.exists (is_free_in id) crossed_types
-                    in
-                    let new_args =
-                      List.fold_left
-                        (fun args (id,rt) ->
-                           List.map (replace_var_by_term id rt) args
-                        )
-                        args
-                        ((id,rt)::new_args)
-                    in
-                    let subst_b =
-                     if is_in_b then b else  replace_var_by_term id rt b
-                    in
-                    let new_env =
-                      let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
-                      let r = Sorts.Relevant in (* TODO relevance *)
-                      EConstr.push_rel (LocalAssum (make_annot n r,t')) env
-                    in
-                    let new_b,id_to_exclude =
-                      rebuild_cons
-                        new_env
-                        nb_args relname
-                        new_args new_crossed_types
-                        (depth + 1) subst_b
-                    in
-                    mkGProd(n,eq',new_b),id_to_exclude
-                end
-                  (* J.F:. keep this comment  it explain how to remove some meaningless equalities
-                     if keep_eq then
-                     mkGProd(n,t,new_b),id_to_exclude
-                     else new_b, Id.Set.add id id_to_exclude
-                  *)
-            | GApp(eq_as_ref,[ty;rt1;rt2])
-                when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous
-                  ->
-              begin
-                try
-                  let l = decompose_raw_eq env rt1 rt2 in
-                  if List.length l > 1
-                  then
-                    let new_rt =
-                      List.fold_left
-                        (fun acc (lhs,rhs) ->
-                          mkGProd(Anonymous,
-                                  mkGApp(mkGRef Coqlib.(lib_ref "core.eq.type"),[mkGHole ();lhs;rhs]),acc)
-                        )
-                        b
-                        l
-                    in
-                    rebuild_cons env nb_args relname args crossed_types depth new_rt
-                  else raise Continue
-              with Continue ->
-                observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
-                let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-                let r = Sorts.Relevant in (* TODO relevance *)
-                let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
-                let new_b,id_to_exclude =
-                  rebuild_cons new_env
-                    nb_args relname
-                    args new_crossed_types
-                    (depth + 1) b
-                in
-                match n with
-                  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
-                      new_b,Id.Set.remove id
-                        (Id.Set.filter not_free_in_t id_to_exclude)
-                  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
-              end
-            | _ ->
-                observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
-                let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-                let r = Sorts.Relevant in (* TODO relevance *)
-                let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
-                let new_b,id_to_exclude =
-                  rebuild_cons new_env
-                    nb_args relname
-                    args new_crossed_types
-                    (depth + 1) b
-                in
-                match n with
-                  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
-                      new_b,Id.Set.remove id
-                        (Id.Set.filter not_free_in_t id_to_exclude)
-                  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
-        end
-    | GLambda(n,k,t,b) ->
-        begin
-          let not_free_in_t id = not (is_free_in id t) in
-          let new_crossed_types = t :: crossed_types in
-          observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt);
-          let t',ctx = Pretyping.understand env (Evd.from_env env) t in
-          match n with
-            | Name id ->
-              let r = Sorts.Relevant in (* TODO relevance *)
-              let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in
-                let new_b,id_to_exclude =
-                  rebuild_cons new_env
-                    nb_args relname
-                    (args@[mkGVar id])new_crossed_types
-                    (depth + 1 ) b
-                in
-                if Id.Set.mem id id_to_exclude && depth >= nb_args
-                then
-                  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
-                else
-                  DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
-            | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
-                (* We have renamed all the anonymous functions during alpha_renaming phase *)
-
-        end
-    | GLetIn(n,v,t,b) ->
-        begin
-          let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
-          let not_free_in_t id = not (is_free_in id t) in
-          let evd = (Evd.from_env env) in
-          let t',ctx = Pretyping.understand env evd t in
-          let evd = Evd.from_ctx ctx in
-          let type_t' = Retyping.get_type_of env evd t' in
-          let t' = EConstr.Unsafe.to_constr t' in
-          let type_t' = EConstr.Unsafe.to_constr type_t' in
-          let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in
-          let new_b,id_to_exclude =
-            rebuild_cons new_env
-              nb_args relname
-              args (t::crossed_types)
-              (depth + 1 ) b in
-          match n with
-            | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
-                new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
-            | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
-                Id.Set.filter not_free_in_t id_to_exclude
-        end
-    | GLetTuple(nal,(na,rto),t,b) ->
-        assert (Option.is_empty rto);
-        begin
-          let not_free_in_t id = not (is_free_in id t) in
-          let new_t,id_to_exclude' =
-            rebuild_cons env
-              nb_args
-              relname
-              args (crossed_types)
-              depth t
-          in
-          let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
-          let r = Sorts.Relevant in (* TODO relevance *)
-          let new_env = EConstr.push_rel (LocalAssum (make_annot na r,t')) env in
-          let new_b,id_to_exclude =
-            rebuild_cons new_env
-              nb_args relname
-              args (t::crossed_types)
-              (depth + 1) b
+  | GProd (n, k, t, b) -> (
+    let not_free_in_t id = not (is_free_in id t) in
+    let new_crossed_types = t :: crossed_types in
+    match DAst.get t with
+    | GApp (res_rt, args') when is_res res_rt -> (
+      let arg = List.hd args' in
+      match DAst.get arg with
+      | GVar this_relname ->
+        (*i The next call to mk_rel_id is
+          valid since we are constructing the graph
+          Ensures by: obvious
+          i*)
+        let new_t =
+          mkGApp (mkGVar (mk_rel_id this_relname), List.tl args' @ [res_rt])
+        in
+        let t', ctx = Pretyping.understand env (Evd.from_env env) new_t in
+        let r = Sorts.Relevant in
+        (* TODO relevance *)
+        let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
+        let new_b, id_to_exclude =
+          rebuild_cons new_env nb_args relname args new_crossed_types
+            (depth + 1) b
+        in
+        (mkGProd (n, new_t, new_b), Id.Set.filter not_free_in_t id_to_exclude)
+      | _ ->
+        (* the first args is the name of the function! *)
+        assert false )
+    | GApp (eq_as_ref, [ty; id; rt])
+      when is_gvar id
+           && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type")
+           && n == Anonymous -> (
+      let loc1 = rt.CAst.loc in
+      let loc2 = eq_as_ref.CAst.loc in
+      let loc3 = id.CAst.loc in
+      let id = match DAst.get id with GVar id -> id | _ -> assert false in
+      try
+        observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt);
+        let t' =
+          try fst (Pretyping.understand env (Evd.from_env env) t) (*FIXME*)
+          with e when CErrors.noncritical e -> raise Continue
+        in
+        let is_in_b = is_free_in id b in
+        let _keep_eq =
+          (not (List.exists (is_free_in id) args))
+          || is_in_b
+          || List.exists (is_free_in id) crossed_types
+        in
+        let new_args = List.map (replace_var_by_term id rt) args in
+        let subst_b = if is_in_b then b else replace_var_by_term id rt b in
+        let r = Sorts.Relevant in
+        (* TODO relevance *)
+        let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
+        let new_b, id_to_exclude =
+          rebuild_cons new_env nb_args relname new_args new_crossed_types
+            (depth + 1) subst_b
+        in
+        (mkGProd (n, t, new_b), id_to_exclude)
+      with Continue ->
+        let jmeq = GlobRef.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
+        let ty', ctx = Pretyping.understand env (Evd.from_env env) ty in
+        let ind, args' =
+          Inductiveops.find_inductive env Evd.(from_env env) ty'
+        in
+        let mib, _ = Global.lookup_inductive (fst ind) in
+        let nparam = mib.Declarations.mind_nparams in
+        let params, arg' = Util.List.chop nparam args' in
+        let rt_typ =
+          DAst.make
+          @@ GApp
+               ( DAst.make @@ GRef (GlobRef.IndRef (fst ind), None)
+               , List.map
+                   (fun p ->
+                     Detyping.detype Detyping.Now false Id.Set.empty env
+                       (Evd.from_env env) (EConstr.of_constr p))
+                   params
+                 @ Array.to_list
+                     (Array.make (List.length args' - nparam) (mkGHole ())) )
+        in
+        let eq' =
+          DAst.make ?loc:loc1
+          @@ GApp
+               ( DAst.make ?loc:loc2 @@ GRef (jmeq, None)
+               , [ty; DAst.make ?loc:loc3 @@ GVar id; rt_typ; rt] )
+        in
+        observe
+          (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
+        let eq'_as_constr, ctx =
+          Pretyping.understand env (Evd.from_env env) eq'
+        in
+        observe (str " computing new type for jmeq : done");
+        let sigma = Evd.(from_env env) in
+        let new_args =
+          match EConstr.kind sigma eq'_as_constr with
+          | App (_, [|_; _; ty; _|]) ->
+            let ty = Array.to_list (snd (EConstr.destApp sigma ty)) in
+            let ty' = snd (Util.List.chop nparam ty) in
+            List.fold_left2
+              (fun acc var_as_constr arg ->
+                if isRel var_as_constr then
+                  let na =
+                    RelDecl.get_name
+                      (Environ.lookup_rel (destRel var_as_constr) env)
+                  in
+                  match na with
+                  | Anonymous -> acc
+                  | Name id' ->
+                    ( id'
+                    , Detyping.detype Detyping.Now false Id.Set.empty env
+                        (Evd.from_env env) arg )
+                    :: acc
+                else if isVar var_as_constr then
+                  ( destVar var_as_constr
+                  , Detyping.detype Detyping.Now false Id.Set.empty env
+                      (Evd.from_env env) arg )
+                  :: acc
+                else acc)
+              [] arg' ty'
+          | _ -> assert false
+        in
+        let is_in_b = is_free_in id b in
+        let _keep_eq =
+          (not (List.exists (is_free_in id) args))
+          || is_in_b
+          || List.exists (is_free_in id) crossed_types
+        in
+        let new_args =
+          List.fold_left
+            (fun args (id, rt) -> List.map (replace_var_by_term id rt) args)
+            args ((id, rt) :: new_args)
+        in
+        let subst_b = if is_in_b then b else replace_var_by_term id rt b in
+        let new_env =
+          let t', ctx = Pretyping.understand env (Evd.from_env env) eq' in
+          let r = Sorts.Relevant in
+          (* TODO relevance *)
+          EConstr.push_rel (LocalAssum (make_annot n r, t')) env
+        in
+        let new_b, id_to_exclude =
+          rebuild_cons new_env nb_args relname new_args new_crossed_types
+            (depth + 1) subst_b
+        in
+        (mkGProd (n, eq', new_b), id_to_exclude)
+      (* J.F:. keep this comment  it explain how to remove some meaningless equalities
+         if keep_eq then
+         mkGProd(n,t,new_b),id_to_exclude
+         else new_b, Id.Set.add id id_to_exclude
+      *) )
+    | GApp (eq_as_ref, [ty; rt1; rt2])
+      when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous
+      -> (
+      try
+        let l = decompose_raw_eq env rt1 rt2 in
+        if List.length l > 1 then
+          let new_rt =
+            List.fold_left
+              (fun acc (lhs, rhs) ->
+                mkGProd
+                  ( Anonymous
+                  , mkGApp
+                      ( mkGRef Coqlib.(lib_ref "core.eq.type")
+                      , [mkGHole (); lhs; rhs] )
+                  , acc ))
+              b l
           in
-(* 	  match n with  *)
-(* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
-(* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
-(* 	    | _ -> *)
-          DAst.make @@ GLetTuple(nal,(na,None),t,new_b),
-                Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
-
-        end
-
-    | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty
-
+          rebuild_cons env nb_args relname args crossed_types depth new_rt
+        else raise Continue
+      with Continue -> (
+        observe
+          (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
+        let t', ctx = Pretyping.understand env (Evd.from_env env) t in
+        let r = Sorts.Relevant in
+        (* TODO relevance *)
+        let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
+        let new_b, id_to_exclude =
+          rebuild_cons new_env nb_args relname args new_crossed_types
+            (depth + 1) b
+        in
+        match n with
+        | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+          (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
+        | _ -> (mkGProd (n, t, new_b), Id.Set.filter not_free_in_t id_to_exclude) )
+      )
+    | _ -> (
+      observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
+      let t', ctx = Pretyping.understand env (Evd.from_env env) t in
+      let r = Sorts.Relevant in
+      (* TODO relevance *)
+      let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
+      let new_b, id_to_exclude =
+        rebuild_cons new_env nb_args relname args new_crossed_types (depth + 1)
+          b
+      in
+      match n with
+      | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+        (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
+      | _ -> (mkGProd (n, t, new_b), Id.Set.filter not_free_in_t id_to_exclude)
+      ) )
+  | GLambda (n, k, t, b) -> (
+    let not_free_in_t id = not (is_free_in id t) in
+    let new_crossed_types = t :: crossed_types in
+    observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt);
+    let t', ctx = Pretyping.understand env (Evd.from_env env) t in
+    match n with
+    | Name id ->
+      let r = Sorts.Relevant in
+      (* TODO relevance *)
+      let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
+      let new_b, id_to_exclude =
+        rebuild_cons new_env nb_args relname
+          (args @ [mkGVar id])
+          new_crossed_types (depth + 1) b
+      in
+      if Id.Set.mem id id_to_exclude && depth >= nb_args then
+        (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
+      else
+        ( DAst.make @@ GProd (n, k, t, new_b)
+        , Id.Set.filter not_free_in_t id_to_exclude )
+    | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
+    (* We have renamed all the anonymous functions during alpha_renaming phase *)
+    )
+  | GLetIn (n, v, t, b) -> (
+    let t =
+      match t with
+      | None -> v
+      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, CastConv t)
+    in
+    let not_free_in_t id = not (is_free_in id t) in
+    let evd = Evd.from_env env in
+    let t', ctx = Pretyping.understand env evd t in
+    let evd = Evd.from_ctx ctx in
+    let type_t' = Retyping.get_type_of env evd t' in
+    let t' = EConstr.Unsafe.to_constr t' in
+    let type_t' = EConstr.Unsafe.to_constr type_t' in
+    let new_env =
+      Environ.push_rel (LocalDef (make_annot n Sorts.Relevant, t', type_t')) env
+    in
+    let new_b, id_to_exclude =
+      rebuild_cons new_env nb_args relname args (t :: crossed_types) (depth + 1)
+        b
+    in
+    match n with
+    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+      (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
+    | _ ->
+      ( DAst.make @@ GLetIn (n, t, None, new_b)
+      , (* HOPING IT WOULD WORK *)
+        Id.Set.filter not_free_in_t id_to_exclude ) )
+  | GLetTuple (nal, (na, rto), t, b) ->
+    assert (Option.is_empty rto);
+    let not_free_in_t id = not (is_free_in id t) in
+    let new_t, id_to_exclude' =
+      rebuild_cons env nb_args relname args crossed_types depth t
+    in
+    let t', ctx = Pretyping.understand env (Evd.from_env env) new_t in
+    let r = Sorts.Relevant in
+    (* TODO relevance *)
+    let new_env = EConstr.push_rel (LocalAssum (make_annot na r, t')) env in
+    let new_b, id_to_exclude =
+      rebuild_cons new_env nb_args relname args (t :: crossed_types) (depth + 1)
+        b
+    in
+    (* 	  match n with  *)
+    (* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
+    (* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
+    (* 	    | _ -> *)
+    ( DAst.make @@ GLetTuple (nal, (na, None), t, new_b)
+    , Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') )
+  | _ -> (mkGApp (mkGVar relname, args @ [rt]), Id.Set.empty)
 
 (* debugging wrapper *)
 let rebuild_cons env nb_args relname args crossed_types rt =
-(*   observennl  (str "rebuild_cons : rt := "++ pr_glob_constr rt ++  *)
-(* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
-  let res =
-    rebuild_cons env nb_args relname args crossed_types 0 rt
-  in
-(*   observe (str " leads to "++ pr_glob_constr (fst res)); *)
+  (*   observennl  (str "rebuild_cons : rt := "++ pr_glob_constr rt ++  *)
+  (* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
+  let res = rebuild_cons env nb_args relname args crossed_types 0 rt in
+  (*   observe (str " leads to "++ pr_glob_constr (fst res)); *)
   res
 
-
 (* naive implementation of parameter detection.
 
    A parameter is an argument which is only preceded by parameters and whose
@@ -1230,92 +1172,103 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 
    TODO: Find a valid way to deal with implicit arguments here!
 *)
-let rec compute_cst_params relnames params gt = DAst.with_val (function
-  | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ | GFloat _ -> params
-  | GApp(f,args) ->
-    begin match DAst.get f with
-    | GVar relname' when Id.Set.mem relname' relnames ->
-      compute_cst_params_from_app [] (params,args)
-    | _ ->
-      List.fold_left (compute_cst_params relnames) params (f::args)
-    end
-  | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) ->
-      let t_params = compute_cst_params relnames params t in
-      compute_cst_params relnames t_params b
-  | GLetIn(_,v,t,b) ->
-      let v_params = compute_cst_params relnames params v in
-      let t_params = Option.fold_left (compute_cst_params relnames) v_params t in
-      compute_cst_params relnames t_params b
-  | GCases _ ->
-      params  (* If there is still cases at this point they can only be
-                 discrimination ones *)
-  | GSort _ -> params
-  | GHole _ -> params
-  | GIf _ | GRec _ | GCast _ ->
-    CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case")
-  ) gt
-and compute_cst_params_from_app acc (params,rtl) =
-  let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in
-  match params,rtl with
-    | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
-    | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c ->
-        compute_cst_params_from_app (param::acc) (params',rtl')
-    | _  -> List.rev acc
-
-let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts =
+let rec compute_cst_params relnames params gt =
+  DAst.with_val
+    (function
+      | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ | GFloat _ -> params
+      | GApp (f, args) -> (
+        match DAst.get f with
+        | GVar relname' when Id.Set.mem relname' relnames ->
+          compute_cst_params_from_app [] (params, args)
+        | _ -> List.fold_left (compute_cst_params relnames) params (f :: args) )
+      | GLambda (_, _, t, b) | GProd (_, _, t, b) | GLetTuple (_, _, t, b) ->
+        let t_params = compute_cst_params relnames params t in
+        compute_cst_params relnames t_params b
+      | GLetIn (_, v, t, b) ->
+        let v_params = compute_cst_params relnames params v in
+        let t_params =
+          Option.fold_left (compute_cst_params relnames) v_params t
+        in
+        compute_cst_params relnames t_params b
+      | GCases _ ->
+        params
+        (* If there is still cases at this point they can only be
+           discrimination ones *)
+      | GSort _ -> params
+      | GHole _ -> params
+      | GIf _ | GRec _ | GCast _ ->
+        CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case"))
+    gt
+
+and compute_cst_params_from_app acc (params, rtl) =
+  let is_gid id c =
+    match DAst.get c with GVar id' -> Id.equal id id' | _ -> false
+  in
+  match (params, rtl) with
+  | _ :: _, [] -> assert false (* the rel has at least nargs + 1 arguments ! *)
+  | ((Name id, _, None) as param) :: params', c :: rtl' when is_gid id c ->
+    compute_cst_params_from_app (param :: acc) (params', rtl')
+  | _ -> List.rev acc
+
+let compute_params_name relnames
+    (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array)
+    csts =
   let rels_params =
     Array.mapi
       (fun i args ->
-         List.fold_left
-           (fun params (_,cst) -> compute_cst_params relnames params cst)
-           args
-           csts.(i)
-      )
+        List.fold_left
+          (fun params (_, cst) -> compute_cst_params relnames params cst)
+          args csts.(i))
       args
   in
   let l = ref [] in
   let _ =
     try
       List.iteri
-        (fun i ((n,nt,typ) as param) ->
-           if Array.for_all
-             (fun l ->
-                let (n',nt',typ') = List.nth l i in
-                Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ')
-             rels_params
-           then
-             l := param::!l
-        )
+        (fun i ((n, nt, typ) as param) ->
+          if
+            Array.for_all
+              (fun l ->
+                let n', nt', typ' = List.nth l i in
+                Name.equal n n' && glob_constr_eq nt nt'
+                && Option.equal glob_constr_eq typ typ')
+              rels_params
+          then l := param :: !l)
         rels_params.(0)
-    with e when CErrors.noncritical e ->
-      ()
+    with e when CErrors.noncritical e -> ()
   in
   List.rev !l
 
 let rec rebuild_return_type rt =
   let loc = rt.CAst.loc in
   match rt.CAst.v with
-    | Constrexpr.CProdN(n,t') ->
-        CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
-    | Constrexpr.CLetIn(na,v,t,t') ->
-        CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
-    | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
-                                       Constrexpr.Default Explicit, rt)],
-                             CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true}))
-
-let do_build_inductive
-      evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
-      returned_types
-      (rtl:glob_constr list) =
+  | Constrexpr.CProdN (n, t') ->
+    CAst.make ?loc @@ Constrexpr.CProdN (n, rebuild_return_type t')
+  | Constrexpr.CLetIn (na, v, t, t') ->
+    CAst.make ?loc @@ Constrexpr.CLetIn (na, v, t, rebuild_return_type t')
+  | _ ->
+    CAst.make ?loc
+    @@ Constrexpr.CProdN
+         ( [ Constrexpr.CLocalAssum
+               ([CAst.make Anonymous], Constrexpr.Default Explicit, rt) ]
+         , CAst.make @@ Constrexpr.CSort (UAnonymous {rigid = true}) )
+
+let do_build_inductive evd (funconstants : pconstant list)
+    (funsargs : (Name.t * glob_constr * glob_constr option) list list)
+    returned_types (rtl : glob_constr list) =
   let _time1 = System.get_time () in
-  let funnames = List.map (fun c -> Label.to_id (KerName.label (Constant.canonical (fst c)))) funconstants in
+  let funnames =
+    List.map
+      (fun c -> Label.to_id (KerName.label (Constant.canonical (fst c))))
+      funconstants
+  in
   (*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
   let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in
   let funnames = Array.of_list funnames in
   let funsargs = Array.of_list funsargs in
   let returned_types = Array.of_list returned_types in
   (* alpha_renaming of the body to prevent variable capture during manipulation *)
-  let rtl_alpha = List.map (function rt ->  expand_as (alpha_rt [] rt)) rtl in
+  let rtl_alpha = List.map (function rt -> expand_as (alpha_rt [] rt)) rtl in
   let rta = Array.of_list rtl_alpha in
   (*i The next call to mk_rel_id is valid since we are constructing the graph
     Ensures by: obvious
@@ -1324,46 +1277,64 @@ let do_build_inductive
   let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in
   (* Construction of the pseudo constructors *)
   let open Context.Named.Declaration in
-  let evd,env =
+  let evd, env =
     Array.fold_right2
-      (fun id (c, u) (evd,env) ->
-       let u = EConstr.EInstance.make u in
-       let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in
-       let t = EConstr.Unsafe.to_constr t in
-       evd,
-       Environ.push_named (LocalAssum (make_annot id Sorts.Relevant,t))
-                         env
-      )
+      (fun id (c, u) (evd, env) ->
+        let u = EConstr.EInstance.make u in
+        let evd, t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in
+        let t = EConstr.Unsafe.to_constr t in
+        ( evd
+        , Environ.push_named (LocalAssum (make_annot id Sorts.Relevant, t)) env
+        ))
       funnames
       (Array.of_list funconstants)
-      (evd,Global.env ())
+      (evd, Global.env ())
   in
   (* we solve and replace the implicits *)
   let rta =
-    Array.mapi (fun i rt ->
-        let _,t = Typing.type_of env evd (EConstr.of_constr (mkConstU ((Array.of_list funconstants).(i)))) in
-        resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt
-      ) rta
+    Array.mapi
+      (fun i rt ->
+        let _, t =
+          Typing.type_of env evd
+            (EConstr.of_constr (mkConstU (Array.of_list funconstants).(i)))
+        in
+        resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env
+          evd rt)
+      rta
   in
   let resa = Array.map (build_entry_lc env evd funnames_as_set []) rta in
   let env_with_graphs =
-    let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
-      let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
+    let rel_arity i funargs =
+      (* Rebuilding arities (with parameters) *)
+      let rel_first_args :
+          (Name.t * Glob_term.glob_constr * Glob_term.glob_constr option) list =
         funargs
       in
       List.fold_right
-        (fun (n,t,typ) acc ->
+        (fun (n, t, typ) acc ->
           match typ with
           | Some typ ->
-             CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
-                              Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
-                              acc)
+            CAst.make
+            @@ Constrexpr.CLetIn
+                 ( CAst.make n
+                 , with_full_print
+                     (Constrextern.extern_glob_constr Id.Set.empty)
+                     t
+                 , Some
+                     (with_full_print
+                        (Constrextern.extern_glob_constr Id.Set.empty)
+                        typ)
+                 , acc )
           | None ->
-             CAst.make @@ Constrexpr.CProdN
-               ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
-                acc
-               )
-        )
+            CAst.make
+            @@ Constrexpr.CProdN
+                 ( [ Constrexpr.CLocalAssum
+                       ( [CAst.make n]
+                       , Constrexpr_ops.default_binder_kind
+                       , with_full_print
+                           (Constrextern.extern_glob_constr Id.Set.empty)
+                           t ) ]
+                 , acc ))
         rel_first_args
         (rebuild_return_type returned_types.(i))
     in
@@ -1372,67 +1343,87 @@ let do_build_inductive
        Then save the graphs and reset Printing options to their primitive values
     *)
     let rel_arities = Array.mapi rel_arity funsargs in
-    Util.Array.fold_left2 (fun env rel_name rel_ar ->
-        let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in
+    Util.Array.fold_left2
+      (fun env rel_name rel_ar ->
+        let rex =
+          fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)
+        in
         let rex = EConstr.Unsafe.to_constr rex in
-        let r = Sorts.Relevant in (* TODO relevance *)
-        Environ.push_named (LocalAssum (make_annot rel_name r,rex)) env) env relnames rel_arities
+        let r = Sorts.Relevant in
+        (* TODO relevance *)
+        Environ.push_named (LocalAssum (make_annot rel_name r, rex)) env)
+      env relnames rel_arities
   in
   (* and of the real constructors*)
   let constr i res =
     List.map
-      (function result (* (args',concl') *) ->
-         let rt = compose_glob_context result.context result.value in
-         let nb_args = List.length funsargs.(i) in
-         (*  with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *)
-         fst (
-           rebuild_cons env_with_graphs nb_args relnames.(i)
-             []
-             []
-             rt
-         )
-      )
+      (function
+        | result (* (args',concl') *) ->
+          let rt = compose_glob_context result.context result.value in
+          let nb_args = List.length funsargs.(i) in
+          (*  with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *)
+          fst (rebuild_cons env_with_graphs nb_args relnames.(i) [] [] rt))
       res.result
   in
   (* adding names to constructors  *)
- let next_constructor_id = ref (-1) in
+  let next_constructor_id = ref (-1) in
   let mk_constructor_id i =
     incr next_constructor_id;
     (*i The next call to mk_rel_id is valid since we are constructing the graph
       Ensures by: obvious
       i*)
-    Id.of_string ((Id.to_string (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
+    Id.of_string
+      ( Id.to_string (mk_rel_id funnames.(i))
+      ^ "_"
+      ^ string_of_int !next_constructor_id )
   in
-  let rel_constructors i rt : (Id.t*glob_constr) list =
-    next_constructor_id := (-1);
-    List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
+  let rel_constructors i rt : (Id.t * glob_constr) list =
+    next_constructor_id := -1;
+    List.map (fun constr -> (mk_constructor_id i, constr)) (constr i rt)
   in
   let rel_constructors = Array.mapi rel_constructors resa in
   (* Computing the set of parameters if asked *)
-  let rels_params = compute_params_name relnames_as_set funsargs  rel_constructors in
+  let rels_params =
+    compute_params_name relnames_as_set funsargs rel_constructors
+  in
   let nrel_params = List.length rels_params in
-  let rel_constructors = (* Taking into account the parameters in constructors *)
-    Array.map (List.map
-    (fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt))))
-    rel_constructors
+  let rel_constructors =
+    (* Taking into account the parameters in constructors *)
+    Array.map
+      (List.map (fun (id, rt) -> (id, snd (chop_rprod_n nrel_params rt))))
+      rel_constructors
   in
-  let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-    let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
-      (snd (List.chop nrel_params funargs))
+  let rel_arity i funargs =
+    (* Reduilding arities (with parameters) *)
+    let rel_first_args :
+        (Name.t * Glob_term.glob_constr * Glob_term.glob_constr option) list =
+      snd (List.chop nrel_params funargs)
     in
     List.fold_right
-      (fun (n,t,typ) acc ->
-         match typ with
-         | Some typ ->
-           CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
-                              Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
-                            acc)
-         | None ->
-           CAst.make @@ Constrexpr.CProdN
-           ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
-            acc
-           )
-      )
+      (fun (n, t, typ) acc ->
+        match typ with
+        | Some typ ->
+          CAst.make
+          @@ Constrexpr.CLetIn
+               ( CAst.make n
+               , with_full_print
+                   (Constrextern.extern_glob_constr Id.Set.empty)
+                   t
+               , Some
+                   (with_full_print
+                      (Constrextern.extern_glob_constr Id.Set.empty)
+                      typ)
+               , acc )
+        | None ->
+          CAst.make
+          @@ Constrexpr.CProdN
+               ( [ Constrexpr.CLocalAssum
+                     ( [CAst.make n]
+                     , Constrexpr_ops.default_binder_kind
+                     , with_full_print
+                         (Constrextern.extern_glob_constr Id.Set.empty)
+                         t ) ]
+               , acc ))
       rel_first_args
       (rebuild_return_type returned_types.(i))
   in
@@ -1443,103 +1434,123 @@ let do_build_inductive
   let rel_arities = Array.mapi rel_arity funsargs in
   let rel_params_ids =
     List.fold_left
-      (fun  acc (na,_,_) ->
-       match na with
-         Anonymous -> acc
-       | Name id -> id::acc
-      )
-      []
-      rels_params
+      (fun acc (na, _, _) ->
+        match na with Anonymous -> acc | Name id -> id :: acc)
+      [] rels_params
   in
   let rel_params =
     List.map
-      (fun (n,t,typ) ->
-         match typ with
-         | Some typ ->
-           Constrexpr.CLocalDef((CAst.make n), Constrextern.extern_glob_constr Id.Set.empty t,
-                                  Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ))
-         | None ->
-         Constrexpr.CLocalAssum
-           ([(CAst.make n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
-      )
+      (fun (n, t, typ) ->
+        match typ with
+        | Some typ ->
+          Constrexpr.CLocalDef
+            ( CAst.make n
+            , Constrextern.extern_glob_constr Id.Set.empty t
+            , Some
+                (with_full_print
+                   (Constrextern.extern_glob_constr Id.Set.empty)
+                   typ) )
+        | None ->
+          Constrexpr.CLocalAssum
+            ( [CAst.make n]
+            , Constrexpr_ops.default_binder_kind
+            , Constrextern.extern_glob_constr Id.Set.empty t ))
       rels_params
   in
   let ext_rels_constructors =
-    Array.map (List.map
-      (fun (id,t) ->
-         false,((CAst.make id),
-                with_full_print
-                  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
-               )
-      ))
-      (rel_constructors)
+    Array.map
+      (List.map (fun (id, t) ->
+           ( false
+           , ( CAst.make id
+             , with_full_print
+                 (Constrextern.extern_glob_type Id.Set.empty)
+                 ((* zeta_normalize *) alpha_rt rel_params_ids t) ) )))
+      rel_constructors
   in
   let rel_ind i ext_rel_constructors =
-    ((CAst.make @@ relnames.(i)),
-    (rel_params,None),
-    Some rel_arities.(i),
-    ext_rel_constructors),[]
+    ( ( CAst.make @@ relnames.(i)
+      , (rel_params, None)
+      , Some rel_arities.(i)
+      , ext_rel_constructors )
+    , [] )
   in
-  let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in
+  let ext_rel_constructors = Array.mapi rel_ind ext_rels_constructors in
   let rel_inds = Array.to_list ext_rel_constructors in
-(*   let _ =  *)
-(*   Pp.msgnl  (\* observe *\) ( *)
-(*       str "Inductive" ++ spc () ++ *)
-(* 	prlist_with_sep  *)
-(* 	(fun () -> fnl ()++spc () ++ str "with" ++ spc ())  *)
-(* 	(function ((_,id),_,params,ar,constr) ->  *)
-(* 	   Ppconstr.pr_id id ++ spc () ++  *)
-(* 	     Ppconstr.pr_binders params ++ spc () ++ *)
-(* 	     str ":" ++ spc () ++  *)
-(* 	     Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *)
-(* 	     prlist_with_sep  *)
-(* 	     (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *)
-(* 	     (function (_,((_,id),t)) ->  *)
-(* 		Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *)
-(* 		  Ppconstr.pr_lconstr_expr t) *)
-(* 	     constr *)
-(* 	) *)
-(* 	rel_inds *)
-(*     ) *)
-(*   in *)
+  (*   let _ =  *)
+  (*   Pp.msgnl  (\* observe *\) ( *)
+  (*       str "Inductive" ++ spc () ++ *)
+  (* 	prlist_with_sep  *)
+  (* 	(fun () -> fnl ()++spc () ++ str "with" ++ spc ())  *)
+  (* 	(function ((_,id),_,params,ar,constr) ->  *)
+  (* 	   Ppconstr.pr_id id ++ spc () ++  *)
+  (* 	     Ppconstr.pr_binders params ++ spc () ++ *)
+  (* 	     str ":" ++ spc () ++  *)
+  (* 	     Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *)
+  (* 	     prlist_with_sep  *)
+  (* 	     (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *)
+  (* 	     (function (_,((_,id),t)) ->  *)
+  (* 		Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *)
+  (* 		  Ppconstr.pr_lconstr_expr t) *)
+  (* 	     constr *)
+  (* 	) *)
+  (* 	rel_inds *)
+  (*     ) *)
+  (*   in *)
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds ~cumulative:false ~poly:false ~private_ind:false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently
+         (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds
+            ~cumulative:false ~poly:false ~private_ind:false
+            ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
-    | UserError(s,msg) as e ->
-        let _time3 = System.get_time () in
-(* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-        let repacked_rel_inds =
-          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn )
-                          rel_inds
-        in
-        let msg =
-          str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
-            ++ fnl () ++
-            msg
-        in
-        observe (msg);
-        raise e
-    | reraise ->
-        let _time3 = System.get_time () in
-(* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-        let repacked_rel_inds =
-          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn )
-                          rel_inds
-        in
-        let msg =
-          str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
-            ++ fnl () ++
-            CErrors.print reraise
-        in
-        observe msg;
-        raise reraise
-
-
+  | UserError (s, msg) as e ->
+    let _time3 = System.get_time () in
+    (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
+    let repacked_rel_inds =
+      List.map
+        (fun ((a, b, c, l), ntn) ->
+          (((false, (a, None)), b, c, Vernacexpr.Constructors l), ntn))
+        rel_inds
+    in
+    let msg =
+      str "while trying to define"
+      ++ spc ()
+      ++ Ppvernac.pr_vernac
+           (CAst.make
+              Vernacexpr.
+                { control = []
+                ; attrs = []
+                ; expr =
+                    VernacInductive (Vernacexpr.Inductive_kw, repacked_rel_inds)
+                })
+      ++ fnl () ++ msg
+    in
+    observe msg; raise e
+  | reraise ->
+    let _time3 = System.get_time () in
+    (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
+    let repacked_rel_inds =
+      List.map
+        (fun ((a, b, c, l), ntn) ->
+          (((false, (a, None)), b, c, Vernacexpr.Constructors l), ntn))
+        rel_inds
+    in
+    let msg =
+      str "while trying to define"
+      ++ spc ()
+      ++ Ppvernac.pr_vernac
+           ( CAst.make
+           @@ Vernacexpr.
+                { control = []
+                ; attrs = []
+                ; expr =
+                    VernacInductive (Vernacexpr.Inductive_kw, repacked_rel_inds)
+                } )
+      ++ fnl () ++ CErrors.print reraise
+    in
+    observe msg; raise reraise
 
 let build_inductive evd funconstants funsargs returned_types rtl =
   let pu = !Detyping.print_universes in