Make Program a regular attribute

We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.

This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.

9 files changed, 358 insertions, 330 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 62c27297f3..ed7c3d6770 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -378,11 +378,11 @@ let is_patvar pat =
   | PatVar _ -> true
   | _ -> false
 
-let coerce_row typing_fun env sigma pats (tomatch,(na,indopt)) =
+let coerce_row ~program_mode typing_fun env sigma pats (tomatch,(na,indopt)) =
   let loc = loc_of_glob_constr tomatch in
   let sigma, tycon, realnames = find_tomatch_tycon !!env sigma loc indopt in
   let sigma, j = typing_fun tycon env sigma tomatch in
-  let sigma, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) !!env sigma j in
+  let sigma, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) ~program_mode !!env sigma j in
   let typ = nf_evar sigma j.uj_type in
   let env = make_return_predicate_ltac_lvar env sigma na tomatch j.uj_val in
   let sigma, t =
@@ -395,12 +395,12 @@ let coerce_row typing_fun env sigma pats (tomatch,(na,indopt)) =
   in
   ((env, sigma), (j.uj_val,t))
 
-let coerce_to_indtype typing_fun env sigma matx tomatchl =
+let coerce_to_indtype ~program_mode typing_fun env sigma matx tomatchl =
   let pats = List.map (fun r ->  r.patterns) matx in
   let matx' = match matrix_transpose pats with
     | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
     | m -> m in
-  let (env, sigma), tms = List.fold_left2_map (fun (env, sigma) -> coerce_row typing_fun env sigma) (env, sigma) matx' tomatchl in
+  let (env, sigma), tms = List.fold_left2_map (fun (env, sigma) -> coerce_row ~program_mode typing_fun env sigma) (env, sigma) matx' tomatchl in
   env, sigma, tms
 
 (************************************************************************)
@@ -410,7 +410,7 @@ let mkExistential ?(src=(Loc.tag Evar_kinds.InternalHole)) env sigma =
   let sigma, (e, u) = Evarutil.new_type_evar env sigma ~src:src univ_flexible_alg in
   sigma, e
 
-let adjust_tomatch_to_pattern sigma pb ((current,typ),deps,dep) =
+let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) =
   (* Ideally, we could find a common inductive type to which both the
      term to match and the patterns coerce *)
   (* In practice, we coerce the term to match if it is not already an
@@ -435,7 +435,7 @@ let adjust_tomatch_to_pattern sigma pb ((current,typ),deps,dep) =
                 | None -> sigma, current
                 | Some sigma -> sigma, current
 	      else
-                let sigma, j = Coercion.inh_conv_coerce_to true !!(pb.env) sigma (make_judge current typ) indt in
+                let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
                 sigma, j.uj_val
             in
             sigma, (current, try_find_ind !!(pb.env) sigma indt names))
@@ -468,10 +468,11 @@ let remove_current_pattern eqn =
 	    alias_stack = alias_of_pat pat :: eqn.alias_stack }
     | [] -> anomaly (Pp.str "Empty list of patterns.")
 
-let push_current_pattern sigma (cur,ty) eqn =
+let push_current_pattern ~program_mode sigma (cur,ty) eqn =
+  let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
   match eqn.patterns with
     | pat::pats ->
-        let _,rhs_env = push_rel sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
+        let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
 	{ eqn with
             rhs = { eqn.rhs with rhs_env = rhs_env };
 	    patterns = pats }
@@ -562,16 +563,17 @@ let occur_in_rhs na rhs =
     | Name id -> Id.Set.mem id rhs.rhs_vars
 
 let is_dep_patt_in eqn pat = match DAst.get pat with
-  | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
+  | PatVar name -> occur_in_rhs name eqn.rhs
   | PatCstr _ -> true
 
-let mk_dep_patt_row (pats,_,eqn) =
-  List.map (is_dep_patt_in eqn) pats
+let mk_dep_patt_row ~program_mode (pats,_,eqn) =
+  if program_mode then List.map (fun _ -> true) pats
+  else List.map (is_dep_patt_in eqn) pats
 
-let dependencies_in_pure_rhs nargs eqns =
+let dependencies_in_pure_rhs ~program_mode nargs eqns =
   if List.is_empty eqns then
-    List.make nargs (not (Flags.is_program_mode ()))  (* Only "_" patts *) else
-  let deps_rows = List.map mk_dep_patt_row eqns in
+    List.make nargs (not program_mode)  (* Only "_" patts *) else
+  let deps_rows = List.map (mk_dep_patt_row ~program_mode) eqns in
   let deps_columns = matrix_transpose deps_rows in
   List.map (List.exists (fun x -> x)) deps_columns
 
@@ -585,10 +587,10 @@ let rec dep_in_tomatch sigma n = function
   | Abstract (_,d) :: l -> RelDecl.exists (fun c -> not (noccurn sigma n c)) d || dep_in_tomatch sigma (n+1) l
   | [] -> false
 
-let dependencies_in_rhs sigma nargs current tms eqns =
+let dependencies_in_rhs ~program_mode sigma nargs current tms eqns =
   match EConstr.kind sigma current with
   | Rel n when dep_in_tomatch sigma n tms -> List.make nargs true
-  | _ -> dependencies_in_pure_rhs nargs eqns
+  | _ -> dependencies_in_pure_rhs ~program_mode nargs eqns
 
 (* Computing the matrix of dependencies *)
 
@@ -788,9 +790,9 @@ let recover_and_adjust_alias_names (_,avoid) names sign =
   in
   List.split (aux (names,sign))
 
-let push_rels_eqn sigma sign eqn =
+let push_rels_eqn ~hypnaming sigma sign eqn =
   {eqn with
-     rhs = {eqn.rhs with rhs_env = snd (push_rel_context sigma sign eqn.rhs.rhs_env) } }
+     rhs = {eqn.rhs with rhs_env = snd (push_rel_context ~hypnaming sigma sign eqn.rhs.rhs_env) } }
 
 let push_rels_eqn_with_names sigma sign eqn =
   let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in
@@ -798,12 +800,12 @@ let push_rels_eqn_with_names sigma sign eqn =
   let sign = recover_initial_subpattern_names subpatnames sign in
   push_rels_eqn sigma sign eqn
 
-let push_generalized_decl_eqn env sigma n decl eqn =
+let push_generalized_decl_eqn ~hypnaming env sigma n decl eqn =
   match RelDecl.get_name decl with
   | Anonymous ->
-      push_rels_eqn sigma [decl] eqn
+      push_rels_eqn ~hypnaming sigma [decl] eqn
   | Name _ ->
-      push_rels_eqn sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
+      push_rels_eqn ~hypnaming sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
 
 let drop_alias_eqn eqn =
   { eqn with alias_stack = List.tl eqn.alias_stack }
@@ -1266,7 +1268,7 @@ let build_leaf sigma pb =
 (* Build the sub-pattern-matching problem for a given branch "C x1..xn as x" *)
 (* spiwack: the [initial] argument keeps track whether the branch is a
    toplevel branch ([true]) or a deep one ([false]). *)
-let build_branch initial current realargs deps (realnames,curname) sigma pb arsign eqns const_info =
+let build_branch ~program_mode initial current realargs deps (realnames,curname) sigma pb arsign eqns const_info =
   (* We remember that we descend through constructor C *)
   let history =
     push_history_pattern const_info.cs_nargs (fst const_info.cs_cstr) pb.history in
@@ -1296,7 +1298,8 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
   let typs' =
     List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in
 
-  let typs,extenv = push_rel_context sigma typs pb.env in
+  let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+  let typs,extenv = push_rel_context ~hypnaming sigma typs pb.env in
 
   let typs' =
     List.map (fun (c,d) ->
@@ -1306,7 +1309,7 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
   (* generalization *)
   let dep_sign =
     find_dependencies_signature sigma
-      (dependencies_in_rhs sigma const_info.cs_nargs current pb.tomatch eqns)
+      (dependencies_in_rhs ~program_mode sigma const_info.cs_nargs current pb.tomatch eqns)
       (List.rev typs') in
 
   (* The dependent term to subst in the types of the remaining UnPushed
@@ -1375,7 +1378,7 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
       tomatch = tomatch;
       pred = pred;
       history = history;
-      mat = List.map (push_rels_eqn_with_names sigma typs) submat }
+      mat = List.map (push_rels_eqn_with_names ~hypnaming sigma typs) submat }
 
 (**********************************************************************
  INVARIANT:
@@ -1390,181 +1393,187 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
 
 (**********************************************************************)
 (* Main compiling descent *)
-let rec compile sigma pb =
-  match pb.tomatch with
-    | Pushed cur :: rest -> match_current sigma { pb with tomatch = rest } cur
-    | Alias (initial,x) :: rest -> compile_alias initial sigma pb x rest
-    | NonDepAlias :: rest -> compile_non_dep_alias sigma pb rest
-    | Abstract (i,d) :: rest -> compile_generalization sigma pb i d rest
-    | [] -> build_leaf sigma pb
+let compile ~program_mode sigma pb =
+  let rec compile sigma pb =
+    match pb.tomatch with
+      | Pushed cur :: rest -> match_current sigma { pb with tomatch = rest } cur
+      | Alias (initial,x) :: rest -> compile_alias initial sigma pb x rest
+      | NonDepAlias :: rest -> compile_non_dep_alias sigma pb rest
+      | Abstract (i,d) :: rest -> compile_generalization sigma pb i d rest
+      | [] -> build_leaf sigma pb
 
 (* Case splitting *)
-and match_current sigma pb (initial,tomatch) =
-  let sigma, tm = adjust_tomatch_to_pattern sigma pb tomatch in
-  let pb,tomatch = adjust_predicate_from_tomatch tomatch tm pb in
-  let ((current,typ),deps,dep) = tomatch in
-  match typ with
-    | NotInd (_,typ) ->
-        check_all_variables !!(pb.env) sigma typ pb.mat;
-        compile_all_variables initial tomatch sigma pb
-    | IsInd (_,(IndType(indf,realargs) as indt),names) ->
+  and match_current sigma pb (initial,tomatch) =
+    let sigma, tm = adjust_tomatch_to_pattern ~program_mode sigma pb tomatch in
+    let pb,tomatch = adjust_predicate_from_tomatch tomatch tm pb in
+    let ((current,typ),deps,dep) = tomatch in
+    match typ with
+      | NotInd (_,typ) ->
+          check_all_variables !!(pb.env) sigma typ pb.mat;
+          compile_all_variables initial tomatch sigma pb
+      | IsInd (_,(IndType(indf,realargs) as indt),names) ->
 	let mind,_ = dest_ind_family indf in
-        let mind = Tacred.check_privacy !!(pb.env) mind in
-        let cstrs = get_constructors !!(pb.env) indf in
-        let arsign, _ = get_arity !!(pb.env) indf in
+          let mind = Tacred.check_privacy !!(pb.env) mind in
+          let cstrs = get_constructors !!(pb.env) indf in
+          let arsign, _ = get_arity !!(pb.env) indf in
 	let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in
-        let no_cstr = Int.equal (Array.length cstrs) 0 in
+          let no_cstr = Int.equal (Array.length cstrs) 0 in
 	if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then
-          compile_all_variables initial tomatch sigma pb
+            compile_all_variables initial tomatch sigma pb
 	else
 	  (* We generalize over terms depending on current term to match *)
-          let pb,deps = generalize_problem (names,dep) sigma pb deps in
+            let pb,deps = generalize_problem (names,dep) sigma pb deps in
 
 	  (* We compile branches *)
-          let fold_br sigma eqn cstr =
-            compile_branch initial current realargs (names,dep) deps sigma pb arsign eqn cstr
-          in
-          let sigma, brvals = Array.fold_left2_map fold_br sigma eqns cstrs in
+            let fold_br sigma eqn cstr =
+              compile_branch initial current realargs (names,dep) deps sigma pb arsign eqn cstr
+            in
+            let sigma, brvals = Array.fold_left2_map fold_br sigma eqns cstrs in
 	  (* We build the (elementary) case analysis *)
-          let depstocheck = current::binding_vars_of_inductive sigma typ in
-          let brvals,tomatch,pred,inst =
-            postprocess_dependencies sigma depstocheck
-              brvals pb.tomatch pb.pred deps cstrs in
-          let brvals = Array.map (fun (sign,body) ->
-            it_mkLambda_or_LetIn body sign) brvals in
+            let depstocheck = current::binding_vars_of_inductive sigma typ in
+            let brvals,tomatch,pred,inst =
+              postprocess_dependencies sigma depstocheck
+                brvals pb.tomatch pb.pred deps cstrs in
+            let brvals = Array.map (fun (sign,body) ->
+              it_mkLambda_or_LetIn body sign) brvals in
 	  let (pred,typ) =
-            find_predicate pb.caseloc pb.env sigma
+              find_predicate pb.caseloc pb.env sigma
 	      pred current indt (names,dep) tomatch in
-          let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in
-          let pred = nf_betaiota !!(pb.env) sigma pred in
+            let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in
+            let pred = nf_betaiota !!(pb.env) sigma pred in
 	  let case =
-            make_case_or_project !!(pb.env) sigma indf ci pred current brvals
+              make_case_or_project !!(pb.env) sigma indf ci pred current brvals
 	  in
-          let sigma, _ = Typing.type_of !!(pb.env) sigma pred in
-          Typing.check_allowed_sort !!(pb.env) sigma mind current pred;
-          sigma, { uj_val = applist (case, inst);
-            uj_type = prod_applist sigma typ inst }
-
-
-(* Building the sub-problem when all patterns are variables. Case
-   where [current] is an intially pushed term. *)
-and shift_problem ((current,t),_,na) sigma pb =
-  let ty = type_of_tomatch t in
-  let tomatch = lift_tomatch_stack 1 pb.tomatch in
-  let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
-  let env = Name.fold_left (fun env id -> hide_variable env Anonymous id) pb.env na in
-  let pb =
-    { pb with
-       env = snd (push_rel sigma (LocalDef (na,current,ty)) env);
-       tomatch = tomatch;
-       pred = lift_predicate 1 pred tomatch;
-       history = pop_history pb.history;
-       mat = List.map (push_current_pattern sigma (current,ty)) pb.mat } in
-  let sigma, j = compile sigma pb in
-  sigma, { uj_val = subst1 current j.uj_val;
-    uj_type = subst1 current j.uj_type }
-
-(* Building the sub-problem when all patterns are variables,
-   non-initial case. Variables which appear as subterms of constructor
-   are already introduced in the context, we avoid creating aliases to
-   themselves by treating this case specially. *)
-and pop_problem ((current,t),_,na) sigma pb =
-  let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
-  let pb =
-    { pb with
-       pred = pred;
-       history = pop_history pb.history;
-       mat = List.map push_noalias_current_pattern pb.mat } in
-  compile sigma pb
+            let sigma, _ = Typing.type_of !!(pb.env) sigma pred in
+            Typing.check_allowed_sort !!(pb.env) sigma mind current pred;
+            sigma, { uj_val = applist (case, inst);
+              uj_type = prod_applist sigma typ inst }
+
+
+  (* Building the sub-problem when all patterns are variables. Case
+     where [current] is an intially pushed term. *)
+  and shift_problem ((current,t),_,na) sigma pb =
+    let ty = type_of_tomatch t in
+    let tomatch = lift_tomatch_stack 1 pb.tomatch in
+    let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
+    let env = Name.fold_left (fun env id -> hide_variable env Anonymous id) pb.env na in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let pb =
+      { pb with
+         env = snd (push_rel ~hypnaming sigma (LocalDef (na,current,ty)) env);
+         tomatch = tomatch;
+         pred = lift_predicate 1 pred tomatch;
+         history = pop_history pb.history;
+         mat = List.map (push_current_pattern ~program_mode sigma (current,ty)) pb.mat } in
+    let sigma, j = compile sigma pb in
+    sigma, { uj_val = subst1 current j.uj_val;
+      uj_type = subst1 current j.uj_type }
+
+  (* Building the sub-problem when all patterns are variables,
+     non-initial case. Variables which appear as subterms of constructor
+     are already introduced in the context, we avoid creating aliases to
+     themselves by treating this case specially. *)
+  and pop_problem ((current,t),_,na) sigma pb =
+    let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
+    let pb =
+      { pb with
+         pred = pred;
+         history = pop_history pb.history;
+         mat = List.map push_noalias_current_pattern pb.mat } in
+    compile sigma pb
 
-(* Building the sub-problem when all patterns are variables. *)
-and compile_all_variables initial cur sigma pb =
-  if initial then shift_problem cur sigma pb
-  else pop_problem cur sigma pb
+  (* Building the sub-problem when all patterns are variables. *)
+  and compile_all_variables initial cur sigma pb =
+    if initial then shift_problem cur sigma pb
+    else pop_problem cur sigma pb
 
-(* Building the sub-problem when all patterns are variables *)
-and compile_branch initial current realargs names deps sigma pb arsign eqns cstr =
-  let sigma, sign, pb = build_branch initial current realargs deps names sigma pb arsign eqns cstr in
-  let sigma, j = compile sigma pb in
-  sigma, (sign, j.uj_val)
+  (* Building the sub-problem when all patterns are variables *)
+  and compile_branch initial current realargs names deps sigma pb arsign eqns cstr =
+    let sigma, sign, pb = build_branch ~program_mode initial current realargs deps names sigma pb arsign eqns cstr in
+    let sigma, j = compile sigma pb in
+    sigma, (sign, j.uj_val)
 
-(* Abstract over a declaration before continuing splitting *)
-and compile_generalization sigma pb i d rest =
-  let pb =
-    { pb with
-       env = snd (push_rel sigma d pb.env);
-       tomatch = rest;
-       mat = List.map (push_generalized_decl_eqn pb.env sigma i d) pb.mat } in
-  let sigma, j = compile sigma pb in
-  sigma, { uj_val = mkLambda_or_LetIn d j.uj_val;
-    uj_type = mkProd_wo_LetIn d j.uj_type }
-
-(* spiwack: the [initial] argument keeps track whether the alias has
-   been introduced by a toplevel branch ([true]) or a deep one
-   ([false]). *)
-and compile_alias initial sigma pb (na,orig,(expanded,expanded_typ)) rest =
-  let f c t =
-    let alias = LocalDef (na,c,t) in
+  (* Abstract over a declaration before continuing splitting *)
+  and compile_generalization sigma pb i d rest =
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
     let pb =
       { pb with
-         env = snd (push_rel sigma alias pb.env);
-         tomatch = lift_tomatch_stack 1 rest;
-         pred = lift_predicate 1 pb.pred pb.tomatch;
-         history = pop_history_pattern pb.history;
-         mat = List.map (push_alias_eqn sigma alias) pb.mat } in
+         env = snd (push_rel ~hypnaming sigma d pb.env);
+         tomatch = rest;
+         mat = List.map (push_generalized_decl_eqn ~hypnaming pb.env sigma i d) pb.mat } in
     let sigma, j = compile sigma pb in
-    sigma, { uj_val =
-        if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then
-          subst1 c j.uj_val
-        else
-          mkLetIn (na,c,t,j.uj_val);
-      uj_type = subst1 c j.uj_type } in
-  (* spiwack: when an alias appears on a deep branch, its non-expanded
-     form is automatically a variable of the same name. We avoid
-     introducing such superfluous aliases so that refines are elegant. *)
-  let just_pop sigma =
+    sigma, { uj_val = mkLambda_or_LetIn d j.uj_val;
+      uj_type = mkProd_wo_LetIn d j.uj_type }
+
+  (* spiwack: the [initial] argument keeps track whether the alias has
+     been introduced by a toplevel branch ([true]) or a deep one
+     ([false]). *)
+  and compile_alias initial sigma pb (na,orig,(expanded,expanded_typ)) rest =
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let f c t =
+      let alias = LocalDef (na,c,t) in
+      let pb =
+        { pb with
+           env = snd (push_rel ~hypnaming sigma alias pb.env);
+           tomatch = lift_tomatch_stack 1 rest;
+           pred = lift_predicate 1 pb.pred pb.tomatch;
+           history = pop_history_pattern pb.history;
+           mat = List.map (push_alias_eqn ~hypnaming sigma alias) pb.mat } in
+      let sigma, j = compile sigma pb in
+      sigma, { uj_val =
+          if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then
+            subst1 c j.uj_val
+          else
+            mkLetIn (na,c,t,j.uj_val);
+        uj_type = subst1 c j.uj_type } in
+    (* spiwack: when an alias appears on a deep branch, its non-expanded
+       form is automatically a variable of the same name. We avoid
+       introducing such superfluous aliases so that refines are elegant. *)
+    let just_pop sigma =
+      let pb =
+        { pb with
+          tomatch = rest;
+          history = pop_history_pattern pb.history;
+          mat = List.map drop_alias_eqn pb.mat } in
+      compile sigma pb
+    in
+    (* If the "match" was orginally over a variable, as in "match x with
+       O => true | n => n end", we give preference to non-expansion in
+       the default clause (i.e. "match x with O => true | n => n end"
+       rather than "match x with O => true | S p => S p end";
+       computationally, this avoids reallocating constructors in cbv
+       evaluation; the drawback is that it might duplicate the instances
+       of the term to match when the corresponding variable is
+       substituted by a non-evaluated expression *)
+    if not program_mode && (isRel sigma orig || isVar sigma orig) then
+      (* Try to compile first using non expanded alias *)
+      try
+        if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
+        else just_pop sigma
+      with e when precatchable_exception e ->
+      (* Try then to compile using expanded alias *)
+      (* Could be needed in case of dependent return clause *)
+      f expanded expanded_typ
+    else
+      (* Try to compile first using expanded alias *)
+      try f expanded expanded_typ
+      with e when precatchable_exception e ->
+      (* Try then to compile using non expanded alias *)
+      (* Could be needed in case of a recursive call which requires to
+         be on a variable for size reasons *)
+      if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
+      else just_pop sigma
+
+
+  (* Remember that a non-trivial pattern has been consumed *)
+  and compile_non_dep_alias sigma pb rest =
     let pb =
       { pb with
-        tomatch = rest;
-        history = pop_history_pattern pb.history;
-        mat = List.map drop_alias_eqn pb.mat } in
+         tomatch = rest;
+         history = pop_history_pattern pb.history;
+         mat = List.map drop_alias_eqn pb.mat } in
     compile sigma pb
   in
-  (* If the "match" was orginally over a variable, as in "match x with
-     O => true | n => n end", we give preference to non-expansion in
-     the default clause (i.e. "match x with O => true | n => n end"
-     rather than "match x with O => true | S p => S p end";
-     computationally, this avoids reallocating constructors in cbv
-     evaluation; the drawback is that it might duplicate the instances
-     of the term to match when the corresponding variable is
-     substituted by a non-evaluated expression *)
-  if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then
-    (* Try to compile first using non expanded alias *)
-    try
-      if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
-      else just_pop sigma
-    with e when precatchable_exception e ->
-    (* Try then to compile using expanded alias *)
-    (* Could be needed in case of dependent return clause *)
-    f expanded expanded_typ
-  else
-    (* Try to compile first using expanded alias *)
-    try f expanded expanded_typ
-    with e when precatchable_exception e ->
-    (* Try then to compile using non expanded alias *)
-    (* Could be needed in case of a recursive call which requires to
-       be on a variable for size reasons *)
-    if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
-    else just_pop sigma
-
-
-(* Remember that a non-trivial pattern has been consumed *)
-and compile_non_dep_alias sigma pb rest =
-  let pb =
-    { pb with
-       tomatch = rest;
-       history = pop_history_pattern pb.history;
-       mat = List.map drop_alias_eqn pb.mat } in
   compile sigma pb
 
 (* pour les alias des initiaux, enrichir les env de ce qu'il faut et
@@ -1650,7 +1659,7 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
   (subst0, t0)
 
 let push_binder sigma d (k,env,subst) =
-  (k+1,snd (push_rel sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
+  (k+1,snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
 
 let rec list_assoc_in_triple x = function
     [] -> raise Not_found
@@ -1771,7 +1780,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t =
  * further explanations
  *)
 
-let build_inversion_problem loc env sigma tms t =
+let build_inversion_problem ~program_mode loc env sigma tms t =
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd !!env sigma t Anonymous) avoid in
     DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in
@@ -1796,13 +1805,13 @@ let build_inversion_problem loc env sigma tms t =
         let patl = pat :: List.rev patl in
         let patl,sign = recover_and_adjust_alias_names acc patl sign in
 	let p = List.length patl in
-        let _,env' = push_rel_context sigma sign env in
+        let _,env' = push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma sign env in
 	let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
 	List.rev_append patl patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
       let pat,acc = make_patvar t acc in
       let d = LocalAssum (alias_of_pat pat,typ) in
-      let patl,acc_sign,acc = aux (n+1) (snd (push_rel sigma d env)) (d::acc_sign) tms acc in
+      let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env)) (d::acc_sign) tms acc in
       pat::patl,acc_sign,acc in
   let avoid0 = GlobEnv.vars_of_env env in
   (* [patl] is a list of patterns revealing the substructure of
@@ -1820,7 +1829,7 @@ let build_inversion_problem loc env sigma tms t =
   let decls =
     List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in
 
-  let _,pb_env = push_rel_context sigma sign env in
+  let _,pb_env = push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma sign env in
   let decls =
     List.map (fun (c,d) -> (c,extract_inductive_data !!(pb_env) sigma d,d)) decls in
 
@@ -1881,7 +1890,7 @@ let build_inversion_problem loc env sigma tms t =
       caseloc   = loc;
       casestyle = RegularStyle;
       typing_function = build_tycon ?loc env pb_env s subst} in
-  let sigma, j = compile sigma pb in
+  let sigma, j = compile ~program_mode sigma pb in
   (sigma, j.uj_val)
 
 (* Here, [pred] is assumed to be in the context built from all *)
@@ -1934,9 +1943,9 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
     | _ -> assert false
   in List.rev (buildrec 0 (tomatchl,tmsign))
 
-let inh_conv_coerce_to_tycon ?loc env sigma j tycon =
+let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon =
   match tycon with
-    | Some p -> Coercion.inh_conv_coerce_to ?loc true env sigma j p
+    | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma j p
     | None -> sigma, j
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
@@ -1953,7 +1962,7 @@ let dependent_rel_or_var sigma tm c =
   | Var id -> Termops.local_occur_var sigma id c
   | _ -> assert false
 
-let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
+let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
   let (rel_subst,var_subst), len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
@@ -2006,7 +2015,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   in
   assert (len == 0);
   let p = predicate 0 c in
-  let arsign,env' = List.fold_right_map (push_rel_context sigma) arsign env in
+  let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+  let arsign,env' = List.fold_right_map (push_rel_context ~hypnaming sigma) arsign env in
   try let sigma' = fst (Typing.type_of !!env' sigma p) in
         Some (sigma', p, arsign)
   with e when precatchable_exception e -> None
@@ -2019,7 +2029,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  * Each matched term is independently considered dependent or not.
  *)
 
-let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
+let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign tycon pred =
   let refresh_tycon sigma t =
     (* If we put the typing constraint in the term, it has to be
        refreshed to preserve the invariant that no algebraic universe
@@ -2041,10 +2051,10 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
              sigma, t in
         (* First strategy: we build an "inversion" predicate, also replacing the *)
         (* dependencies with existential variables *)
-        let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+        let sigma1,pred1 = build_inversion_problem loc ~program_mode env sigma tomatchs t in
         (* Optional second strategy: we abstract the tycon wrt to the dependencies *)
         let p2 =
-          prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
+          prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign t in
         (* Third strategy: we take the type constraint as it is; of course we could *)
         (* need something inbetween, abstracting some but not all of the dependencies *)
         (* the "inversion" strategy deals with that but unification may not be *)
@@ -2060,7 +2070,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
     (* Some type annotation *)
     | Some rtntyp ->
       (* We extract the signature of the arity *)
-      let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in
+      let building_arsign,envar = List.fold_right_map (push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma) arsign env in
       let sigma, newt = new_sort_variable univ_flexible sigma in
       let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in
       let predccl = nf_evar sigma predcclj.uj_val in
@@ -2320,7 +2330,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity =
 	 in
          let sigma, ineqs = build_ineqs sigma prevpatterns pats signlen in
          let rhs_rels' = rels_of_patsign sigma rhs_rels in
-         let _signenv,_ = push_rel_context sigma rhs_rels' env in
+         let _signenv,_ = push_rel_context ~hypnaming:ProgramNaming sigma rhs_rels' env in
 	 let arity =
 	   let args, nargs =
 	     List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
@@ -2340,7 +2350,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity =
            let eqs_rels, arity = decompose_prod_n_assum sigma neqs arity in
 	     eqs_rels @ neqs_rels @ rhs_rels', arity
 	 in
-         let _,rhs_env = push_rel_context sigma rhs_rels' env in
+         let _,rhs_env = push_rel_context ~hypnaming:ProgramNaming sigma rhs_rels' env in
          let sigma, j = typing_fun (mk_tycon tycon) rhs_env sigma eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
@@ -2518,10 +2528,10 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let env, sigma, tomatchs = coerce_to_indtype typing_function env sigma matx tomatchl in
+  let env, sigma, tomatchs = coerce_to_indtype ~program_mode:true typing_function env sigma matx tomatchl in
   let tycon = valcon_of_tycon tycon in
   let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env sigma tomatchs tycon in
-  let _,env = push_rel_context sigma tomatchs_lets env in
+  let _,env = push_rel_context ~hypnaming:ProgramNaming sigma tomatchs_lets env in
   let len = List.length eqns in
   let sigma, sign, allnames, signlen, eqs, neqs, args =
     (* The arity signature *)
@@ -2540,7 +2550,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
       sigma, ev, lift nar ev
     | Some t ->
         let sigma, pred =
-          match prepare_predicate_from_arsign_tycon env sigma loc tomatchs sign t with
+          match prepare_predicate_from_arsign_tycon ~program_mode:true env sigma loc tomatchs sign t with
           | Some (evd, pred, arsign) -> evd, pred
           | None -> sigma, lift nar t
         in
@@ -2557,7 +2567,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
   in
   let matx = List.rev matx in
   let _ = assert (Int.equal len (List.length lets)) in
-  let _,env = push_rel_context sigma lets env in
+  let _,env = push_rel_context ~hypnaming:ProgramNaming sigma lets env in
   let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
   let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
   let args = List.rev_map (lift len) args in
@@ -2604,7 +2614,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
       casestyle= style;
       typing_function = typing_function } in
 
-  let sigma, j = compile sigma pb in
+  let sigma, j = compile ~program_mode:true sigma pb in
     (* We check for unused patterns *)
     List.iter (check_unused_pattern !!env) matx;
     let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
@@ -2617,8 +2627,8 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
 
-let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, eqns) =
-  if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then
+let compile_cases ?loc ~program_mode style (typing_fun, sigma) tycon env (predopt, tomatchl, eqns) =
+  if predopt == None && program_mode && Program.is_program_cases () then
     compile_program_cases ?loc style (typing_fun, sigma)
       tycon env (predopt, tomatchl, eqns)
   else
@@ -2628,13 +2638,13 @@ let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, e
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let predenv, sigma, tomatchs = coerce_to_indtype typing_fun env sigma matx tomatchl in
+  let predenv, sigma, tomatchs = coerce_to_indtype ~program_mode typing_fun env sigma matx tomatchl in
 
   (* If an elimination predicate is provided, we check it is compatible
      with the type of arguments to match; if none is provided, we
      build alternative possible predicates *)
   let arsign = extract_arity_signature !!env tomatchs tomatchl in
-  let preds = prepare_predicate ?loc typing_fun predenv sigma tomatchs arsign tycon predopt in
+  let preds = prepare_predicate ?loc ~program_mode typing_fun predenv sigma tomatchs arsign tycon predopt in
 
   let compile_for_one_predicate (sigma,nal,pred) =
     (* We push the initial terms to match and push their alias to rhs' envs *)
@@ -2679,10 +2689,10 @@ let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, e
 	casestyle = style;
 	typing_function = typing_fun } in
 
-    let sigma, j = compile sigma pb in
+    let sigma, j = compile ~program_mode sigma pb in
 
     (* We coerce to the tycon (if an elim predicate was provided) *)
-    inh_conv_coerce_to_tycon ?loc !!env sigma j tycon
+    inh_conv_coerce_to_tycon ?loc ~program_mode !!env sigma j tycon
   in
 
   (* Return the term compiled with the first possible elimination  *)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 36cfa0a70d..b0349a3d05 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -40,7 +40,7 @@ val irrefutable : env -> cases_pattern -> bool
 (** {6 Compilation primitive. } *)
 
 val compile_cases :
-  ?loc:Loc.t -> case_style ->
+  ?loc:Loc.t -> program_mode:bool -> case_style ->
   (type_constraint -> GlobEnv.t -> evar_map -> glob_constr -> evar_map * unsafe_judgment) * evar_map ->
   type_constraint ->
   GlobEnv.t -> glob_constr option * tomatch_tuples * cases_clauses ->
@@ -111,9 +111,9 @@ type 'a pattern_matching_problem =
       casestyle : case_style;
       typing_function: type_constraint -> GlobEnv.t -> evar_map -> 'a option -> evar_map * unsafe_judgment }
 
-val compile : evar_map -> 'a pattern_matching_problem -> evar_map * unsafe_judgment
+val compile : program_mode:bool -> evar_map -> 'a pattern_matching_problem -> evar_map * unsafe_judgment
 
-val prepare_predicate : ?loc:Loc.t ->
+val prepare_predicate : ?loc:Loc.t -> program_mode:bool ->
            (type_constraint ->
             GlobEnv.t -> Evd.evar_map -> glob_constr -> Evd.evar_map * unsafe_judgment) ->
            GlobEnv.t ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 4d1d405bd7..9e93c470b1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -393,7 +393,7 @@ let apply_coercion env sigma p hj typ_cl =
   with NoCoercion as e -> raise e
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
-let inh_app_fun_core env evd j =
+let inh_app_fun_core ~program_mode env evd j =
   let t = whd_all env evd j.uj_type in
     match EConstr.kind evd t with
     | Prod (_,_,_) -> (evd,j)
@@ -404,25 +404,25 @@ let inh_app_fun_core env evd j =
       	try let t,p =
 	  lookup_path_to_fun_from env evd j.uj_type in
 	    apply_coercion env evd p j t
-	with Not_found | NoCoercion ->
-          if Flags.is_program_mode () then
-	  try
-	    let evdref = ref evd in
-	    let coercef, t = mu env evdref t in
-	    let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
-	      (!evdref, res)
-	  with NoSubtacCoercion | NoCoercion ->
-	    (evd,j)
-          else raise NoCoercion
+       with Not_found | NoCoercion ->
+         if program_mode then
+           try
+             let evdref = ref evd in
+             let coercef, t = mu env evdref t in
+             let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
+             (!evdref, res)
+           with NoSubtacCoercion | NoCoercion ->
+             (evd,j)
+         else raise NoCoercion
 
 (* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
-let inh_app_fun resolve_tc env evd j =
-  try inh_app_fun_core env evd j
+let inh_app_fun ~program_mode resolve_tc env evd j =
+  try inh_app_fun_core ~program_mode env evd j
   with
   | NoCoercion when not resolve_tc
     || not (get_use_typeclasses_for_conversion ()) -> (evd, j)
   | NoCoercion ->
-    try inh_app_fun_core env (saturate_evd env evd) j
+    try inh_app_fun_core ~program_mode env (saturate_evd env evd) j
     with NoCoercion -> (evd, j)
 
 let type_judgment env sigma j =
@@ -449,8 +449,8 @@ let inh_coerce_to_sort ?loc env evd j =
     | _ ->
 	inh_tosort_force ?loc env evd j
 
-let inh_coerce_to_base ?loc env evd j =
-  if Flags.is_program_mode () then
+let inh_coerce_to_base ?loc ~program_mode env evd j =
+  if program_mode then
     let evdref = ref evd in
     let ct, typ' = mu env evdref j.uj_type in
     let res =
@@ -459,8 +459,8 @@ let inh_coerce_to_base ?loc env evd j =
     in !evdref, res
   else (evd, j)
 
-let inh_coerce_to_prod ?loc env evd t =
-  if Flags.is_program_mode () then
+let inh_coerce_to_prod ?loc ~program_mode env evd t =
+  if program_mode then
     let evdref = ref evd in
     let _, typ' = mu env evdref t in
       !evdref, typ'
@@ -520,13 +520,13 @@ let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 =
       | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
 
 (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t =
+let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly env evd cj t =
   let (evd', val') =
     try
       inh_conv_coerce_to_fail ?loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
     with NoCoercionNoUnifier (best_failed_evd,e) ->
       try
-	if Flags.is_program_mode () then
+        if program_mode then
 	  coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t
 	else raise NoSubtacCoercion
       with
@@ -545,9 +545,11 @@ let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t =
   let val' = match val' with Some v -> v | None -> assert(false) in
     (evd',{ uj_val = val'; uj_type = t })
 
-let inh_conv_coerce_to ?loc resolve_tc = inh_conv_coerce_to_gen ?loc resolve_tc false
+let inh_conv_coerce_to ?loc ~program_mode resolve_tc =
+  inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false
 
-let inh_conv_coerce_rigid_to ?loc resolve_tc = inh_conv_coerce_to_gen resolve_tc ?loc true
+let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc =
+  inh_conv_coerce_to_gen ~program_mode resolve_tc ?loc true
 
 let inh_conv_coerces_to ?loc env evd t t' =
   try
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 6cfd958b46..a941391125 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -21,7 +21,7 @@ open Glob_term
     type a product; it returns [j] if no coercion is applicable.
     resolve_tc=false disables resolving type classes (as the last
     resort before failing) *)
-val inh_app_fun : bool ->
+val inh_app_fun : program_mode:bool -> bool ->
   env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
 (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
@@ -33,11 +33,11 @@ val inh_coerce_to_sort : ?loc:Loc.t ->
 (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
     type its base type (the notion depends on the coercion system) *)
-val inh_coerce_to_base : ?loc:Loc.t ->
+val inh_coerce_to_base : ?loc:Loc.t -> program_mode:bool ->
   env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
 (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
-val inh_coerce_to_prod : ?loc:Loc.t ->
+val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool ->
   env -> evar_map -> types -> evar_map * types
 
 (** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an 
@@ -45,10 +45,10 @@ val inh_coerce_to_prod : ?loc:Loc.t ->
     a way [t] and [j.uj_type] are convertible; it fails if no coercion is
     applicable. resolve_tc=false disables resolving type classes (as the last
     resort before failing) *)
-val inh_conv_coerce_to : ?loc:Loc.t -> bool ->
+val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool ->
   env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
-val inh_conv_coerce_rigid_to : ?loc:Loc.t -> bool ->
+val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool ->
   env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
 (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 49a08afe80..d6b204561e 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -38,10 +38,10 @@ type t = {
   lvar : ltac_var_map;
 }
 
-let make env sigma lvar =
+let make ~hypnaming env sigma lvar =
   let get_extra env sigma =
     let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
-    Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
+    Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
       (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
   {
     static_env = env;
@@ -66,32 +66,32 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id =
 
 let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar)
 
-let push_rel sigma d env =
+let push_rel ~hypnaming sigma d env =
   let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
   let env = {
     static_env = push_rel d env.static_env;
     renamed_env = push_rel d' env.renamed_env;
-    extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra));
+    extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
   d', env
 
-let push_rel_context ?(force_names=false) sigma ctx env =
+let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
   let open Context.Rel.Declaration in
   let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in
   let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in
   let env = {
     static_env = push_rel_context ctx env.static_env;
     renamed_env = push_rel_context ctx' env.renamed_env;
-    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra));
+    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
   ctx', env
 
-let push_rec_types sigma (lna,typarray) env =
+let push_rec_types ~hypnaming sigma (lna,typarray) env =
   let open Context.Rel.Declaration in
   let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
-  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in
+  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e ~hypnaming in (e,d)) env ctxt in
   Array.map get_name ctx, env
 
 let new_evar env sigma ?src ?naming typ =
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index e8a2fbdd16..63f72e60bd 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -13,6 +13,7 @@ open Environ
 open Evd
 open EConstr
 open Ltac_pretype
+open Evarutil
 
 (** To embed constr in glob_constr *)
 
@@ -37,7 +38,7 @@ type t
 
 (** Build a pretyping environment from an ltac environment *)
 
-val make : env -> evar_map -> ltac_var_map -> t
+val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
 
 (** Export the underlying environement *)
 
@@ -47,9 +48,9 @@ val vars_of_env : t -> Id.Set.t
 
 (** Push to the environment, returning the declaration(s) with interpreted names *)
 
-val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t
-val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
-val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t array * t
+val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t
+val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
+val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t array * constr array -> t -> Name.t array * t
 
 (** Declare an evar using renaming information *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 57705fa209..46e463512d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -190,7 +190,8 @@ type inference_flags = {
   use_typeclasses : bool;
   solve_unification_constraints : bool;
   fail_evar : bool;
-  expand_evars : bool
+  expand_evars : bool;
+  program_mode : bool;
 }
 
 (* Compute the set of still-undefined initial evars up to restriction
@@ -226,17 +227,17 @@ let frozen_and_pending_holes (sigma, sigma') =
     end in
     FrozenProgress data
 
-let apply_typeclasses env sigma frozen fail_evar =
+let apply_typeclasses ~program_mode env sigma frozen fail_evar =
   let filter_frozen = match frozen with
     | FrozenId map -> fun evk -> Evar.Map.mem evk map
     | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
   in
   let sigma = Typeclasses.resolve_typeclasses
-      ~filter:(if Flags.is_program_mode ()
+      ~filter:(if program_mode
                then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
                else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk)))
       ~split:true ~fail:fail_evar env sigma in
-  let sigma = if Flags.is_program_mode () then (* Try optionally solving the obligations *)
+  let sigma = if program_mode then (* Try optionally solving the obligations *)
       Typeclasses.resolve_typeclasses
         ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env sigma
     else sigma in
@@ -264,9 +265,9 @@ let apply_heuristics env sigma fail_evar =
     let e = CErrors.push e in
     if fail_evar then iraise e else sigma
 
-let check_typeclasses_instances_are_solved env current_sigma frozen =
+let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
-  apply_typeclasses env current_sigma frozen true
+  apply_typeclasses ~program_mode env current_sigma frozen true
 
 let check_extra_evars_are_solved env current_sigma frozen = match frozen with
 | FrozenId _ -> ()
@@ -295,18 +296,19 @@ let check_evars env initial_sigma sigma c =
     | _ -> EConstr.iter sigma proc_rec c
   in proc_rec c
 
-let check_evars_are_solved env sigma frozen =
-  let sigma = check_typeclasses_instances_are_solved env sigma frozen in
+let check_evars_are_solved ~program_mode env sigma frozen =
+  let sigma = check_typeclasses_instances_are_solved ~program_mode env sigma frozen in
   check_problems_are_solved env sigma;
   check_extra_evars_are_solved env sigma frozen
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
 let solve_remaining_evars ?hook flags env ?initial sigma =
+  let program_mode = flags.program_mode in
   let frozen = frozen_and_pending_holes (initial, sigma) in
   let sigma =
     if flags.use_typeclasses
-    then apply_typeclasses env sigma frozen false
+    then apply_typeclasses ~program_mode env sigma frozen false
     else sigma
   in
   let sigma = match hook with
@@ -317,12 +319,12 @@ let solve_remaining_evars ?hook flags env ?initial sigma =
     then apply_heuristics env sigma false
     else sigma
   in
-  if flags.fail_evar then check_evars_are_solved env sigma frozen;
+  if flags.fail_evar then check_evars_are_solved ~program_mode env sigma frozen;
   sigma
 
-let check_evars_are_solved env ?initial current_sigma =
+let check_evars_are_solved ~program_mode env ?initial current_sigma =
   let frozen = frozen_and_pending_holes (initial, current_sigma) in
-  check_evars_are_solved env current_sigma frozen
+  check_evars_are_solved ~program_mode env current_sigma frozen
 
 let process_inference_flags flags env initial (sigma,c,cty) =
   let sigma = solve_remaining_evars flags env ~initial sigma in
@@ -351,10 +353,10 @@ let adjust_evar_source sigma na c =
   | _, _ -> sigma, c
 
 (* coerce to tycon if any *)
-let inh_conv_coerce_to_tycon ?loc resolve_tc env sigma j = function
+let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = function
   | None -> sigma, j
   | Some t ->
-    Coercion.inh_conv_coerce_to ?loc resolve_tc !!env sigma j t
+    Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t
 
 let check_instance loc subst = function
   | [] -> ()
@@ -453,20 +455,18 @@ let new_type_evar env sigma loc =
   new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
 
 let mark_obligation_evar sigma k evc =
-  if Flags.is_program_mode () then
-    match k with
-    | Evar_kinds.QuestionMark _
-    | Evar_kinds.ImplicitArg (_, _, false) ->
-      Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
-    | _ -> sigma
-  else sigma
+  match k with
+  | Evar_kinds.QuestionMark _
+  | Evar_kinds.ImplicitArg (_, _, false) ->
+    Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
+  | _ -> sigma
 
 (* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [sigma] and *)
 (* the type constraint tycon *)
 
-let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
-  let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in
+let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
+  let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in
   let pretype_type = pretype_type k0 resolve_tc in
   let pretype = pretype k0 resolve_tc in
   let open Context.Rel.Declaration in
@@ -477,7 +477,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
     inh_conv_coerce_to_tycon ?loc env sigma t_ref tycon
 
   | GVar id ->
-    let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) k0 loc env sigma id in
+    let sigma, t_id = pretype_id (fun e r t -> pretype ~program_mode tycon e r t) k0 loc env sigma id in
     inh_conv_coerce_to_tycon ?loc env sigma t_id tycon
 
   | GEvar (id, inst) ->
@@ -488,7 +488,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         try Evd.evar_key id sigma
         with Not_found -> error_evar_not_found ?loc !!env sigma id in
       let hyps = evar_filtered_context (Evd.find sigma evk) in
-      let sigma, args = pretype_instance k0 resolve_tc env sigma loc hyps evk inst in
+      let sigma, args = pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = Retyping.get_judgment_of !!env sigma c in
       inh_conv_coerce_to_tycon ?loc env sigma j tycon
@@ -513,7 +513,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         | Some ty -> sigma, ty
         | None -> new_type_evar env sigma loc in
       let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
-      let sigma = mark_obligation_evar sigma k uj_val in
+      let sigma = if program_mode then mark_obligation_evar sigma k uj_val else sigma in
       sigma, { uj_val; uj_type = ty }
 
   | GHole (k, _naming, Some arg) ->
@@ -525,24 +525,25 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       sigma, { uj_val = c; uj_type = ty }
 
   | GRec (fixkind,names,bl,lar,vdef) ->
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
     let rec type_bl env sigma ctxt = function
       | [] -> sigma, ctxt
       | (na,bk,None,ty)::bl ->
-        let sigma, ty' = pretype_type empty_valcon env sigma ty in
-	let dcl = LocalAssum (na, ty'.utj_val) in
-        let dcl', env = push_rel sigma dcl env in
+        let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in
+        let dcl = LocalAssum (na, ty'.utj_val) in
+        let dcl', env = push_rel ~hypnaming sigma dcl env in
         type_bl env sigma (Context.Rel.add dcl' ctxt) bl
       | (na,bk,Some bd,ty)::bl ->
-        let sigma, ty' = pretype_type empty_valcon env sigma ty in
-        let sigma, bd' = pretype (mk_tycon ty'.utj_val) env sigma bd in
+        let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in
+        let sigma, bd' = pretype ~program_mode (mk_tycon ty'.utj_val) env sigma bd in
         let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
-        let dcl', env = push_rel sigma dcl env in
+        let dcl', env = push_rel ~hypnaming sigma dcl env in
         type_bl env sigma (Context.Rel.add dcl' ctxt) bl in
     let sigma, ctxtv = Array.fold_left_map (fun sigma -> type_bl env sigma Context.Rel.empty) sigma bl in
     let sigma, larj =
       Array.fold_left2_map
         (fun sigma e ar ->
-          pretype_type empty_valcon (snd (push_rel_context sigma e env)) sigma ar)
+          pretype_type ~program_mode empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar)
         sigma ctxtv lar in
     let lara = Array.map (fun a -> a.utj_val) larj in
     let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
@@ -562,7 +563,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       | None -> sigma
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
-    let names,newenv = push_rec_types sigma (names,ftys) env in
+    let names,newenv = push_rec_types ~hypnaming sigma (names,ftys) env in
     let sigma, vdefj =
       Array.fold_left2_map_i
         (fun i sigma ctxt def ->
@@ -571,8 +572,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
            let (ctxt,ty) =
              decompose_prod_n_assum sigma (Context.Rel.length ctxt)
                (lift nbfix ftys.(i)) in
-           let ctxt,nenv = push_rel_context sigma ctxt newenv in
-           let sigma, j = pretype (mk_tycon ty) nenv sigma def in
+           let ctxt,nenv = push_rel_context ~hypnaming sigma ctxt newenv in
+           let sigma, j = pretype ~program_mode (mk_tycon ty) nenv sigma def in
            sigma, { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
                     uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         sigma ctxtv vdef in
@@ -618,14 +619,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
     inh_conv_coerce_to_tycon ?loc env sigma j tycon
 
   | GApp (f,args) ->
-    let sigma, fj = pretype empty_tycon env sigma f in
+    let sigma, fj = pretype ~program_mode empty_tycon env sigma f in
     let floc = loc_of_glob_constr f in
     let length = List.length args in
     let candargs =
 	(* Bidirectional typechecking hint: 
 	   parameters of a constructor are completely determined
 	   by a typing constraint *)
-      if Flags.is_program_mode () && length > 0 && isConstruct sigma fj.uj_val then
+      if program_mode && length > 0 && isConstruct sigma fj.uj_val then
 	match tycon with
 	| None -> []
 	| Some ty ->
@@ -656,12 +657,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       | [] -> sigma, resj
       | c::rest ->
         let argloc = loc_of_glob_constr c in
-        let sigma, resj = Coercion.inh_app_fun resolve_tc !!env sigma resj in
+        let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in
         let resty = whd_all !!env sigma resj.uj_type in
         match EConstr.kind sigma resty with
         | Prod (na,c1,c2) ->
           let tycon = Some c1 in
-          let sigma, hj = pretype tycon env sigma c in
+          let sigma, hj = pretype ~program_mode tycon env sigma c in
           let sigma, candargs, ujval =
             match candargs with
             | [] -> sigma, [], j_val hj
@@ -678,7 +679,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	    let j = { uj_val = value; uj_type = typ } in
             apply_rec env sigma (n+1) j candargs rest
 	  | _ ->
-            let sigma, hj = pretype empty_tycon env sigma c in
+            let sigma, hj = pretype ~program_mode empty_tycon env sigma c in
 	      error_cant_apply_not_functional
                 ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|]
     in
@@ -703,29 +704,31 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       match tycon with
       | None -> sigma, tycon
       | Some ty ->
-        let sigma, ty' = Coercion.inh_coerce_to_prod ?loc !!env sigma ty in
+        let sigma, ty' = Coercion.inh_coerce_to_prod ?loc ~program_mode !!env sigma ty in
         sigma, Some ty'
     in
     let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in
     let dom_valcon = valcon_of_tycon dom in
-    let sigma, j = pretype_type dom_valcon env sigma c1 in
+    let sigma, j = pretype_type ~program_mode dom_valcon env sigma c1 in
     let var = LocalAssum (name, j.utj_val) in
-    let var',env' = push_rel sigma var env in
-    let sigma, j' = pretype rng env' sigma c2 in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let var',env' = push_rel ~hypnaming sigma var env in
+    let sigma, j' = pretype ~program_mode rng env' sigma c2 in
     let name = get_name var' in
     let resj = judge_of_abstraction !!env (orelse_name name name') j j' in
     inh_conv_coerce_to_tycon ?loc env sigma resj tycon
 
   | GProd(name,bk,c1,c2) ->
-    let sigma, j = pretype_type empty_valcon env sigma c1 in
+    let sigma, j = pretype_type ~program_mode empty_valcon env sigma c1 in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
     let sigma, name, j' = match name with
       | Anonymous ->
-        let sigma, j = pretype_type empty_valcon env sigma c2 in
+        let sigma, j = pretype_type ~program_mode empty_valcon env sigma c2 in
         sigma, name, { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
         let var = LocalAssum (name, j.utj_val) in
-        let var, env' = push_rel sigma var env in
-        let sigma, c2_j = pretype_type empty_valcon env' sigma c2 in
+        let var, env' = push_rel ~hypnaming sigma var env in
+        let sigma, c2_j = pretype_type ~program_mode empty_valcon env' sigma c2 in
         sigma, get_name var, c2_j
     in
     let resj =
@@ -741,23 +744,24 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
     let sigma, tycon1 =
       match t with
       | Some t ->
-        let sigma, t_j = pretype_type empty_valcon env sigma t in
+        let sigma, t_j = pretype_type ~program_mode empty_valcon env sigma t in
         sigma, mk_tycon t_j.utj_val
       | None ->
         sigma, empty_tycon in
-    let sigma, j = pretype tycon1 env sigma c1 in
+    let sigma, j = pretype ~program_mode tycon1 env sigma c1 in
     let sigma, t = Evarsolve.refresh_universes
       ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma j.uj_type in
     let var = LocalDef (name, j.uj_val, t) in
     let tycon = lift_tycon 1 tycon in
-    let var, env = push_rel sigma var env in
-    let sigma, j' = pretype tycon env sigma c2 in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let var, env = push_rel ~hypnaming sigma var env in
+    let sigma, j' = pretype ~program_mode tycon env sigma c2 in
     let name = get_name var in
     sigma, { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
              uj_type = subst1 j.uj_val j'.uj_type }
 
   | GLetTuple (nal,(na,po),c,d) ->
-    let sigma, cj = pretype empty_tycon env sigma c in
+    let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
     let (IndType (indf,realargs)) =
       try find_rectype !!env sigma cj.uj_type
       with Not_found ->
@@ -792,7 +796,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	  | _ -> assert false
 	in aux 1 1 (List.rev nal) cs.cs_args, true in
     let fsign = Context.Rel.map (whd_betaiota sigma) fsign in
-    let fsign,env_f = push_rel_context sigma fsign env in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in
     let obj ind p v f =
       if not record then
 	let f = it_mkLambda_or_LetIn f fsign in
@@ -810,10 +815,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
       let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in
       let nar = List.length arsgn in
-      let psign',env_p = push_rel_context ~force_names:true sigma psign predenv in
+      let psign',env_p = push_rel_context ~hypnaming ~force_names:true sigma psign predenv in
 	  (match po with
 	  | Some p ->
-            let sigma, pj = pretype_type empty_valcon env_p sigma p in
+            let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in
             let ccl = nf_evar sigma pj.utj_val in
 	    let p = it_mkLambda_or_LetIn ccl psign' in
 	    let inst =
@@ -821,7 +826,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	      @[EConstr.of_constr (build_dependent_constructor cs)] in
 	    let lp = lift cs.cs_nargs p in
             let fty = hnf_lam_applist !!env sigma lp inst in
-            let sigma, fj = pretype (mk_tycon fty) env_f sigma d in
+            let sigma, fj = pretype ~program_mode (mk_tycon fty) env_f sigma d in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
                 Typing.check_allowed_sort !!env sigma ind cj.uj_val p;
@@ -831,7 +836,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 
 	  | None ->
 	    let tycon = lift_tycon cs.cs_nargs tycon in
-            let sigma, fj = pretype tycon env_f sigma d in
+            let sigma, fj = pretype ~program_mode tycon env_f sigma d in
             let ccl = nf_evar sigma fj.uj_type in
 	    let ccl =
               if noccur_between sigma 1 cs.cs_nargs ccl then
@@ -848,7 +853,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
             in sigma, { uj_val = v; uj_type = ccl })
 
   | GIf (c,(na,po),b1,b2) ->
-    let sigma, cj = pretype empty_tycon env sigma c in
+    let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
     let (IndType (indf,realargs)) =
       try find_rectype !!env sigma cj.uj_type
       with Not_found ->
@@ -869,10 +874,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
       let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
       let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in
-      let psign,env_p = push_rel_context sigma psign predenv in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+      let psign,env_p = push_rel_context ~hypnaming sigma psign predenv in
       let sigma, pred, p = match po with
 	| Some p ->
-          let sigma, pj = pretype_type empty_valcon env_p sigma p in
+          let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in
           let ccl = nf_evar sigma pj.utj_val in
           let pred = it_mkLambda_or_LetIn ccl psign in
           let typ = lift (- nar) (beta_applist sigma (pred,[cj.uj_val])) in
@@ -894,8 +900,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	let csgn =
           List.map (set_name Anonymous) cs_args
         in
-        let _,env_c = push_rel_context sigma csgn env in
-        let sigma, bj = pretype (mk_tycon pi) env_c sigma b in
+        let _,env_c = push_rel_context ~hypnaming sigma csgn env in
+        let sigma, bj = pretype ~program_mode (mk_tycon pi) env_c sigma b in
         sigma, it_mkLambda_or_LetIn bj.uj_val cs_args in
       let sigma, b1 = f sigma cstrs.(0) b1 in
       let sigma, b2 = f sigma cstrs.(1) b2 in
@@ -910,23 +916,23 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       inh_conv_coerce_to_tycon ?loc env sigma cj tycon
 
   | GCases (sty,po,tml,eqns) ->
-    Cases.compile_cases ?loc sty (pretype, sigma) tycon env (po,tml,eqns)
+    Cases.compile_cases ?loc ~program_mode sty (pretype ~program_mode, sigma) tycon env (po,tml,eqns)
 
   | GCast (c,k) ->
     let sigma, cj =
       match k with
       | CastCoerce ->
-        let sigma, cj = pretype empty_tycon env sigma c in
-        Coercion.inh_coerce_to_base ?loc !!env sigma cj
+        let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
+        Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj
       | CastConv t | CastVM t | CastNative t ->
         let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
-        let sigma, tj = pretype_type empty_valcon env sigma t in
+        let sigma, tj = pretype_type ~program_mode empty_valcon env sigma t in
         let sigma, tval = Evarsolve.refresh_universes
             ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma tj.utj_val in
         let tval = nf_evar sigma tval in
         let (sigma, cj), tval = match k with
 	  | VMcast ->
-            let sigma, cj = pretype empty_tycon env sigma c in
+            let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
             let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in
               if not (occur_existential sigma cty || occur_existential sigma tval) then
                 match Reductionops.vm_infer_conv !!env sigma cty tval with
@@ -937,7 +943,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	      else user_err ?loc  (str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
-            let sigma, cj = pretype empty_tycon env sigma c in
+            let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
             let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in
             begin
               match Nativenorm.native_infer_conv !!env sigma cty tval with
@@ -947,7 +953,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
                   (ConversionFailed (!!env,cty,tval))
             end
           | _ ->
-            pretype (mk_tycon tval) env sigma c, tval
+            pretype ~program_mode (mk_tycon tval) env sigma c, tval
         in
         let v = mkCast (cj.uj_val, k, tval) in
         sigma, { uj_val = v; uj_type = tval }
@@ -961,7 +967,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         in
         inh_conv_coerce_to_tycon ?loc env sigma resj tycon
 
-and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
+and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
   let f decl (subst,update,sigma) =
     let id = NamedDecl.get_id decl in
     let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
@@ -993,7 +999,7 @@ and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
     let sigma, c, update =
       try
         let c = List.assoc id update in
-        let sigma, c = pretype k0 resolve_tc (mk_tycon t) env sigma c in
+        let sigma, c = pretype ~program_mode k0 resolve_tc (mk_tycon t) env sigma c in
         check_body sigma id (Some c.uj_val);
         sigma, c.uj_val, List.remove_assoc id update
       with Not_found ->
@@ -1018,7 +1024,7 @@ and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
   sigma, Array.map_of_list snd subst
 
 (* [pretype_type valcon env sigma c] coerces [c] into a type *)
-and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
+and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
   | GHole (knd, naming, None) ->
       let loc = loc_of_glob_constr c in
       (match valcon with
@@ -1042,10 +1048,10 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
        | None ->
          let sigma, s = new_sort_variable univ_flexible_alg sigma in
          let sigma, utj_val = new_evar env sigma ~src:(loc, knd) ~naming (mkSort s) in
-         let sigma = mark_obligation_evar sigma knd utj_val in
+         let sigma = if program_mode then mark_obligation_evar sigma knd utj_val else sigma in
          sigma, { utj_val; utj_type = s})
   | _ ->
-      let sigma, j = pretype k0 resolve_tc empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode k0 resolve_tc empty_tycon env sigma c in
       let loc = loc_of_glob_constr c in
       let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in
 	match valcon with
@@ -1059,17 +1065,21 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
           end
 
 let ise_pretype_gen flags env sigma lvar kind c =
-  let env = GlobEnv.make env sigma lvar in
+  let program_mode = flags.program_mode in
+  let hypnaming =
+    if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
+  in
+  let env = GlobEnv.make ~hypnaming env sigma lvar in
   let k0 = Context.Rel.length (rel_context !!env) in
   let sigma', c', c'_ty = match kind with
     | WithoutTypeConstraint ->
-      let sigma, j = pretype k0 flags.use_typeclasses empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode k0 flags.use_typeclasses empty_tycon env sigma c in
       sigma, j.uj_val, j.uj_type
     | OfType exptyp ->
-      let sigma, j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+      let sigma, j = pretype ~program_mode k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
       sigma, j.uj_val, j.uj_type
     | IsType ->
-      let sigma, tj = pretype_type k0 flags.use_typeclasses empty_valcon env sigma c in
+      let sigma, tj = pretype_type ~program_mode k0 flags.use_typeclasses empty_valcon env sigma c in
       sigma, tj.utj_val, mkSort tj.utj_type
   in
   process_inference_flags flags !!env sigma (sigma',c',c'_ty)
@@ -1078,13 +1088,17 @@ let default_inference_flags fail = {
   use_typeclasses = true;
   solve_unification_constraints = true;
   fail_evar = fail;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 let no_classes_no_fail_inference_flags = {
   use_typeclasses = false;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 59e6c00037..3c875e69d2 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -36,7 +36,8 @@ type inference_flags = {
   use_typeclasses : bool;
   solve_unification_constraints : bool;
   fail_evar : bool;
-  expand_evars : bool
+  expand_evars : bool;
+  program_mode : bool;
 }
 
 val default_inference_flags : bool -> inference_flags
@@ -101,7 +102,7 @@ val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
     reporting an appropriate error message *)
 
 val check_evars_are_solved :
-  env -> ?initial:evar_map -> (* current map: *) evar_map -> unit
+  program_mode:bool -> env -> ?initial:evar_map -> (* current map: *) evar_map -> unit
 
 (** [check_evars env initial_sigma extended_sigma c] fails if some
    new unresolved evar remains in [c] *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e4d96da0a6..ac0b58b92b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1269,7 +1269,7 @@ let is_mimick_head sigma ts f =
 
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
-  let (evd',j') = inh_conv_coerce_rigid_to true env evd j tycon in
+  let (evd',j') = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in
   let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
   let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in
     (evd',j'.uj_val)