Merge branch 'trunk' into located_switch

1 files changed, 15 insertions, 5 deletions

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index f0883e286..331b025f0 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -8,7 +8,7 @@ open Declare
 (**
    - Get types of existentials ;
    - Flatten dependency tree (prefix order) ;
-   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
+   - Replace existentials by de Bruijn indices in term, applied to the right arguments ;
    - Apply term prefixed by quantification on "existentials".
 *)
 
@@ -51,7 +51,7 @@ type oblinfo =
     ev_tac: unit Proofview.tactic option;
     ev_deps: Int.Set.t }
 
-(** Substitute evar references in t using De Bruijn indices,
+(** Substitute evar references in t using de Bruijn indices,
   where n binders were passed through. *)
 
 let subst_evar_constr evs n idf t =
@@ -102,7 +102,7 @@ let subst_evar_constr evs n idf t =
     t', !seen, !transparent
 
 
-(** Substitute variable references in t using De Bruijn indices,
+(** Substitute variable references in t using de Bruijn indices,
   where n binders were passed through. *)
 let subst_vars acc n t =
   let var_index id = Util.List.index Id.equal id acc in
@@ -630,6 +630,16 @@ let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 let add_hint local prg cst =
   Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
 
+let it_mkLambda_or_LetIn_or_clean t ctx =
+  let open Context.Rel.Declaration in
+  let fold t decl =
+    if is_local_assum decl then mkLambda_or_LetIn decl t
+    else
+      if noccurn 1 t then subst1 mkProp t
+      else mkLambda_or_LetIn decl t
+  in
+  Context.Rel.fold_inside fold ctx ~init:t
+
 let declare_obligation prg obl body ty uctx =
   let body = prg.prg_reduce body in
   let ty = Option.map prg.prg_reduce ty in
@@ -663,7 +673,7 @@ let declare_obligation prg obl body ty uctx =
 	    if poly then
 	      Some (DefinedObl constant)
 	    else
-	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
+	      Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
 
 let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
 		   notations obls impls kind reduce hook =
@@ -1087,7 +1097,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
       Defined cst)
   else (
     let len = Array.length obls in
-    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
+    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
       progmap_add n (CEphemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with