Coq: use `abstract` to separate out proofs from definitions

- requires fixpoint definitions containing proofs to be processed in proof
  mode (due to a bug in Coq), so change libraries and pretty printing to
  do that
- adjust some lemmas to avoid extra evars

6 files changed, 132 insertions, 76 deletions

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 1aaa3298..698ca51b 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -107,7 +107,7 @@ Qed.
 Lemma subrange_lemma2 {n m o} : (o <= m < n -> m+1 = o+(m-o+1))%nat.
 omega.
 Qed.
-Lemma subrange_lemma3 {n m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} :
+Lemma subrange_lemma3 {m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m)} :
   Z.of_nat (Z.to_nat m - Z.to_nat o + 1)%nat = m - o + 1.
 unwrap_ArithFacts.
 rewrite Nat2Z.inj_add.
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index d2a8c805..fbc0f5b1 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -30,21 +30,25 @@ match l with
   foreachM xs vars body
 end.
 
-Fixpoint foreach_ZM_up' {rv e Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e :=
+Fixpoint foreach_ZM_up' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e.
+exact (
   if sumbool_of_bool (from + off <=? to) then
     match n with
     | O => returnm vars
-    | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_up' from to step (off + step) n vars body
+    | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_up' rv e Vars from to step (off + step) n _ _ vars body
     end
-  else returnm vars.
+  else returnm vars).
+Defined.
 
-Fixpoint foreach_ZM_down' {rv e Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e :=
+Fixpoint foreach_ZM_down' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e.
+exact (
   if sumbool_of_bool (to <=? from + off) then
     match n with
     | O => returnm vars
-    | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_down' from to step (off - step) n vars body
+    | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_down' _ _ _ from to step (off - step) n _ _ vars body
     end
-  else returnm vars.
+  else returnm vars).
+Defined.
 
 Definition foreach_ZM_up {rv e Vars} from to step vars body `{ArithFact (0 < step)} :=
     foreach_ZM_up' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
@@ -190,13 +194,15 @@ Definition Zwf_guarded (z:Z) : Acc (Zwf 0) z :=
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
-Fixpoint whileMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E :=
+Fixpoint whileMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E.
+exact (
   if Z_ge_dec limit 0 then
     cond vars >>= fun cond_val =>
     if cond_val then
-      body vars >>= fun vars => whileMT' (limit - 1) vars cond body (_limit_reduces acc)
+      body vars >>= fun vars => whileMT' _ _ _ (limit - 1) vars cond body (_limit_reduces acc)
     else returnm vars
-  else Fail "Termination limit reached".
+  else Fail "Termination limit reached").
+Defined.
 
 Definition whileMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
   let limit := measure vars in
@@ -204,12 +210,14 @@ Definition whileMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars
 
 (*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
-Fixpoint untilMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E :=
+Fixpoint untilMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E.
+exact (
   if Z_ge_dec limit 0 then
     body vars >>= fun vars =>
     cond vars >>= fun cond_val =>
-    if cond_val then returnm vars else untilMT' (limit - 1) vars cond body (_limit_reduces acc)
-  else Fail "Termination limit reached".
+    if cond_val then returnm vars else untilMT' _ _ _ (limit - 1) vars cond body (_limit_reduces acc)
+  else Fail "Termination limit reached").
+Defined.
 
 Definition untilMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
   let limit := measure vars in
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v
index 7a25cbe9..618ca3a5 100644
--- a/lib/coq/Sail2_state.v
+++ b/lib/coq/Sail2_state.v
@@ -114,13 +114,15 @@ let rec untilS vars cond body s =
   if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
 *)
 
-Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E :=
+Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E.
+exact (
   if Z_ge_dec limit 0 then
     cond vars >>$= fun cond_val =>
     if cond_val then
-      body vars >>$= fun vars => whileST' (limit - 1) vars cond body (_limit_reduces acc)
+      body vars >>$= fun vars => whileST' _ _ _ (limit - 1) vars cond body (_limit_reduces acc)
     else returnS vars
-  else failS "Termination limit reached".
+  else failS "Termination limit reached").
+Defined.
 
 Definition whileST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
   let limit := measure vars in
@@ -128,12 +130,14 @@ Definition whileST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV b
 
 (*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
-Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E :=
+Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E.
+exact (
   if Z_ge_dec limit 0 then
     body vars >>$= fun vars =>
     cond vars >>$= fun cond_val =>
-    if cond_val then returnS vars else untilST' (limit - 1) vars cond body (_limit_reduces acc)
-  else failS "Termination limit reached".
+    if cond_val then returnS vars else untilST' _ _ _ (limit - 1) vars cond body (_limit_reduces acc)
+  else failS "Termination limit reached").
+Defined.
 
 Definition untilST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
   let limit := measure vars in
diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
index 90ae6840..dd83f239 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -839,26 +839,26 @@ unfold whileMT, whileST.
 generalize (measure vars) as limit. intro.
 revert vars.
 destruct (Z.le_decidable 0 limit).
-* generalize (Zwf_guarded limit) as acc.
+* generalize (Zwf_guarded limit) at 1 as acc1.
+  generalize (Zwf_guarded limit) at 1 as acc2.
   apply Wf_Z.natlike_ind with (x := limit).
-  + intros [acc] *; simpl.
-    match goal with |- context [Build_ArithFact _ ?prf] => generalize prf; intros ?Proof end.
+  + intros [acc1] [acc2] *; simpl.
     rewrite_liftState.
     apply bindS_cong; auto.
     intros [|]; auto.
     apply bindS_cong; auto.
-    intros. destruct (_limit_reduces _). simpl.
+    intros. repeat destruct (_limit_reduces _). simpl.
     reflexivity.
   + clear limit H.
-    intros limit H IH [acc] vars s. simpl.
+    intros limit H IH [acc1] [acc2] vars s. simpl.
     destruct (Z_ge_dec _ _); try omega.
     rewrite_liftState.
     apply bindS_cong; auto.
     intros [|]; auto.
     apply bindS_cong; auto.
     intros.
-    gen_reduces.
-    replace (Z.succ limit - 1) with limit; try omega. intro acc'.
+    repeat gen_reduces.
+    replace (Z.succ limit - 1) with limit; try omega. intros acc1' acc2'.
     apply IH.
   + assumption.
 * intros. simpl.
@@ -912,24 +912,25 @@ unfold untilMT, untilST.
 generalize (measure vars) as limit. intro.
 revert vars.
 destruct (Z.le_decidable 0 limit).
-* generalize (Zwf_guarded limit) as acc.
+* generalize (Zwf_guarded limit) at 1 as acc1.
+  generalize (Zwf_guarded limit) at 1 as acc2.
   apply Wf_Z.natlike_ind with (x := limit).
-  + intros [acc] * s; simpl.
+  + intros [acc1] [acc2] * s; simpl.
     rewrite_liftState.
     apply bindS_cong; auto.
     intros. apply bindS_cong; auto.
     intros [|]; auto.
-    destruct (_limit_reduces _). simpl.
+    repeat destruct (_limit_reduces _). simpl.
     reflexivity.
   + clear limit H.
-    intros limit H IH [acc] vars s. simpl.
+    intros limit H IH [acc1] [acc2] vars s. simpl.
     destruct (Z_ge_dec _ _); try omega.
     rewrite_liftState.
     apply bindS_cong; auto.
     intros. apply bindS_cong; auto.
     intros [|]; auto.
-    gen_reduces.
-    replace (Z.succ limit - 1) with limit; try omega. intro acc'.
+    repeat gen_reduces.
+    replace (Z.succ limit - 1) with limit; try omega. intros acc1' acc2'.
     apply IH.
   + assumption.
 * intros. simpl.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index afa22856..47fa2fda 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1785,18 +1785,9 @@ Ltac solve_unknown :=
     exact (Build_ArithFact _ I)
   end.
 
-Ltac solve_arithfact :=
+Ltac run_main_solver_impl :=
 (* Attempt a simple proof first to avoid lengthy preparation steps (especially
    as the large proof terms can upset subsequent proofs). *)
-intros; (* To solve implications for derive_m *)
-try solve_unknown;
-match goal with |- ArithFact (?x <= ?x <= ?x) => try (exact trivial_range) | _ => idtac end;
-try fill_in_evar_eq;
-try match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end;
-(* Trying reflexivity will fill in more complex metavariable examples than
-   fill_in_evar_eq above, e.g., 8 * n = 8 * ?Goal3 *)
-try (constructor; reflexivity);
-try (constructor; repeat match goal with |- and _ _ => split end; z_comparisons);
 try (constructor; simple_omega);
 prepare_for_solver;
 (*dump_context;*)
@@ -1804,9 +1795,31 @@ constructor;
 repeat match goal with |- and _ _ => split end;
 main_solver.
 
+(* This can be redefined to remove the abstract. *)
+Ltac run_main_solver :=
+  solve
+    [ abstract run_main_solver_impl
+    | run_main_solver_impl (* for cases where there's an evar in the goal *)
+    ].
+
+Ltac solve_arithfact :=
+  intros; (* To solve implications for derive_m *)
+  solve
+    [ solve_unknown
+    | match goal with |- ArithFact (?x <= ?x <= ?x) => exact trivial_range end
+    | fill_in_evar_eq
+    | match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end
+    (* Trying reflexivity will fill in more complex metavariable examples than
+       fill_in_evar_eq above, e.g., 8 * n = 8 * ?Goal3 *)
+    | constructor; reflexivity
+    | constructor; repeat match goal with |- and _ _ => split end; z_comparisons
+    | run_main_solver
+    ].
+
 (* Add an indirection so that you can redefine run_solver to fail to get
    slow running constraints into proof mode. *)
 Ltac run_solver := solve_arithfact.
+
 Hint Extern 0 (ArithFact _) => run_solver : typeclass_instances.
 
 Hint Unfold length_mword : sail.
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index b0a0aee8..b8bbe8aa 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -98,7 +98,7 @@ type context = {
   kid_id_renames_rev : kid Bindings.t; (* reverse of kid_id_renames *)
   bound_nvars : KidSet.t;
   build_at_return : string option;
-  recursive_ids : IdSet.t;
+  recursive_fns : (int * int) Bindings.t; (* Number of implicit arguments and constraints for (mutually) recursive definitions *)
   debug : bool;
 }
 let empty_ctxt = {
@@ -108,7 +108,7 @@ let empty_ctxt = {
   kid_id_renames_rev = Bindings.empty;
   bound_nvars = KidSet.empty;
   build_at_return = None;
-  recursive_ids = IdSet.empty;
+  recursive_fns = Bindings.empty;
   debug = false;
 }
 
@@ -1773,12 +1773,11 @@ let doc_exp, doc_let =
           let env = env_of_annot (l,annot) in
           let () = debug ctxt (lazy ("Function application " ^ string_of_id f)) in
           let call, is_extern, is_ctor, is_rec =
-            if Env.is_union_constructor f env then doc_id_ctor f, false, true, false else
+            if Env.is_union_constructor f env then doc_id_ctor f, false, true, None else
             if Env.is_extern f env "coq"
-            then string (Env.get_extern f env "coq"), true, false, false
-            else if IdSet.mem f ctxt.recursive_ids
-            then doc_id f, false, false, true
-            else doc_id f, false, false, false in
+            then string (Env.get_extern f env "coq"), true, false, None
+            else doc_id f, false, false, Bindings.find_opt f ctxt.recursive_fns
+          in
           let (tqs,fn_ty) =
             if is_ctor then Env.get_union_id f env else Env.get_val_spec f env
           in
@@ -1880,14 +1879,17 @@ let doc_exp, doc_let =
             if is_ctor
             then group (hang 2 (call ^^ break 1 ^^ parens (flow (comma ^^ break 1) (List.map2 (doc_arg false) args arg_typs))))
             else
-              let main_call = call :: List.map2 (doc_arg true) args arg_typs in
+              let argspp = List.map2 (doc_arg true) args arg_typs in
               let all =
-                if is_rec then main_call @
-                                 [parens (string "_limit_reduces _acc")]
-                else match f with
-                     | Id_aux (Id x,_) when is_prefix "#rec#" x ->
-                        main_call @ [parens (string "Zwf_guarded _")]
-                     | _ ->  main_call
+                match is_rec with
+                | Some (pre,post) -> call :: List.init pre (fun _ -> underscore) @ argspp @
+                                       List.init post (fun _ -> underscore) @
+                                         [parens (string "_limit_reduces _acc")]
+                | None -> 
+                   match f with
+                   | Id_aux (Id x,_) when is_prefix "#rec#" x ->
+                      call :: argspp @ [parens (string "Zwf_guarded _")]
+                   | _ -> call :: argspp
               in hang 2 (flow (break 1) all) in
 
           (* Decide whether to unpack an existential result, pack one, or cast.
@@ -2852,7 +2854,7 @@ let merge_var_patterns map pats =
 
 type mutrec_pos = NotMutrec | FirstFn | LaterFn
 
-let doc_funcl mutrec rec_opt ?rec_set (FCL_aux(FCL_Funcl(id, pexp), annot)) =
+let doc_funcl_init mutrec rec_opt ?rec_set (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let env = env_of_annot annot in
   let (tq,typ) = Env.get_val_spec_orig id env in
   let (arg_typs, ret_typ, eff) = match typ with
@@ -2874,10 +2876,9 @@ let doc_funcl mutrec rec_opt ?rec_set (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let pats, eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in
   let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in
   let kids_used = KidSet.diff bound_kids eliminated_kids in
-  let is_measured, recursive_ids = match rec_opt with
-    | Rec_aux (Rec_measure _,_) ->
-       true, (match rec_set with None -> IdSet.singleton id | Some s -> s)
-    | _ -> false, IdSet.empty
+  let is_measured = match rec_opt with
+    | Rec_aux (Rec_measure _,_) -> true
+    | _ -> false
   in
   let kir_rev =
     KBindings.fold
@@ -2891,7 +2892,7 @@ let doc_funcl mutrec rec_opt ?rec_set (FCL_aux(FCL_Funcl(id, pexp), annot)) =
       kid_id_renames_rev = kir_rev;
       bound_nvars = bound_kids;
       build_at_return = None; (* filled in below *)
-      recursive_ids = recursive_ids;
+      recursive_fns = Bindings.empty; (* filled in later *)
       debug = List.mem (string_of_id id) (!opt_debug_on)
     } in
   let build_ex, ret_typ = replace_atom_return_type ret_typ in
@@ -2960,7 +2961,6 @@ let doc_funcl mutrec rec_opt ?rec_set (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   in
   let patspp = flow_map (break 1) doc_binder pats in
   let atom_constrs = Util.map_filter (atom_constraint ctxt) pats in
-  let atom_constr_pp = separate space atom_constrs in
   let retpp =
     (* TODO: again, probably should provide proper environment *)
     if effectful eff
@@ -3012,18 +3012,29 @@ let doc_funcl mutrec rec_opt ?rec_set (FCL_aux(FCL_Funcl(id, pexp), annot)) =
       ^^ dot
     else empty
   in
+  let ctxt =
+    if is_measured then
+      { ctxt with recursive_fns =
+                    Bindings.singleton id
+                      (List.length quantspp, List.length constrspp + List.length atom_constrs) }
+    else ctxt in
   let _ = match guard with
     | None -> ()
     | _ ->
        raise (Reporting.err_unreachable l __POS__
                "guarded pattern expression should have been rewritten before pretty-printing") in
+  ((group (flow (break 1) ([intropp; idpp] @ quantspp @ [patspp] @ constrspp @ atom_constrs @ accpp) ^/^
+      flow (break 1) (measurepp @ [colon; retpp])),
+    implicitargs),
+   ctxt,
+   (exp, eff, build_ex, fixupspp))
+
+
+let doc_funcl_body ctxt (exp, eff, build_ex, fixupspp) =
   let bodypp = doc_fun_body ctxt exp in
   let bodypp = if effectful eff then bodypp else match build_ex with Some s -> string s ^^ parens bodypp | None -> bodypp in
   let bodypp = separate (break 1) fixupspp ^/^ bodypp in
-  group (prefix 3 1
-    (flow (break 1) ([intropp; idpp] @ quantspp @ [patspp] @ constrspp @ [atom_constr_pp] @ accpp) ^/^
-       flow (break 1) (measurepp @ [colon; retpp; coloneq]))
-    (bodypp ^^ terminalpp)) ^^ implicitargs
+  group bodypp
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
@@ -3035,22 +3046,45 @@ let get_id = function
 let doc_fundef_rhs ?(mutrec=NotMutrec) rec_set (FD_aux(FD_function(r, typa, efa, funcls),(l,_))) =
   match funcls with
   | [] -> unreachable l __POS__ "function with no clauses"
-  | [funcl] -> doc_funcl mutrec r ~rec_set funcl
+  | [funcl] -> doc_funcl_init mutrec r ~rec_set funcl
   | (FCL_aux (FCL_Funcl (id,_),_))::_ -> unreachable l __POS__ ("function " ^ string_of_id id ^ " has multiple clauses in backend")
 
 let doc_mutrec rec_set = function
   | [] -> failwith "DEF_internal_mutrec with empty function list"
   | fundef::fundefs ->
-     doc_fundef_rhs ~mutrec:FirstFn rec_set fundef ^^ hardline ^^
-     separate_map hardline (doc_fundef_rhs ~mutrec:LaterFn rec_set) fundefs ^^ dot
+     let prepost1,ctxt1,details1 = doc_fundef_rhs ~mutrec:FirstFn rec_set fundef in
+     let prepostn,ctxtn,detailsn = Util.split3 (List.map (doc_fundef_rhs ~mutrec:LaterFn rec_set) fundefs) in
+     let recursive_fns = List.fold_left (fun m c -> Bindings.union (fun _ x _ -> Some x) m c.recursive_fns) ctxt1.recursive_fns ctxtn in
+     let ctxts = List.map (fun c -> { c with recursive_fns }) (ctxt1::ctxtn) in
+     let bodies = List.map2 doc_funcl_body ctxts (details1::detailsn) in
+     let bodies = List.map (fun b -> string "exact (" ^/^ b ^/^ string ").") bodies in
+     let pres, posts = List.split (prepost1::prepostn) in
+     separate hardline pres ^^ dot ^^ hardline ^^
+       separate hardline bodies ^^
+         break 1 ^^ string "Defined." ^^ hardline ^^
+           separate hardline posts
+
+let doc_funcl mutrec r funcl =
+  let (pre,post),ctxt,details = doc_funcl_init mutrec r funcl in
+  let body = doc_funcl_body ctxt details in
+  pre,body,post
 
 let rec doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),fannot)) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
   | [FCL_aux (FCL_Funcl(id,_),annot) as funcl]
     when not (Env.is_extern id (env_of_annot annot) "coq") ->
-     doc_funcl NotMutrec r funcl
-  | [_] -> empty (* extern *)
+     begin
+       let pre,body,post = doc_funcl NotMutrec r funcl in
+       match r with
+       | Rec_aux (Rec_measure _,_) ->
+          group (pre ^^ dot ^^ hardline ^^
+                   string "exact (" ^^ hardline ^^
+                     body ^^
+                       string ")." ^^ hardline ^^ string "Defined.") ^^ hardline ^^ post
+       | _ -> group (prefix 3 1 (pre ^^ space ^^ coloneq) (body ^^ dot)) ^^ post
+     end
+   | [_] -> empty (* extern *)
   | _ -> failwith "FD_function with more than one clause"
 
 
@@ -3349,14 +3383,10 @@ try
         hardline;
         string "Open Scope string."; hardline;
         string "Open Scope bool."; hardline;
-        (* Put the body into a Section so that we can define some values with
-           Let to put them into the local context, where tactics can see them *)
-        string "Section Content.";
         hardline;
         hardline;
         separate empty (List.map doc_def defs);
         hardline;
-        string "End Content.";
         hardline])
 with Type_check.Type_error (env,l,err) ->
   let extra =