From 20642607f48d8c4ac8978c0f0f17e14bfa9bd335 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 May 2019 18:43:03 +0200
Subject: Impargs: Using ExplByPos/ExplByName rather than encoding index as an
 ident.

This moves the encoding of "n" as "arg_n" closer to the user interface level.

Note however that Constrintern.build_impl is not able yet to use ExplByPos.
See further commits.
---
 vernac/comProgramFixpoint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0e17f2b274..d48e2139d1 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -200,7 +200,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
         Constrintern.Recursive full_arity impls
     in
     let newimpls = Id.Map.singleton recname
-        (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
+        (r, l, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
          scopes @ [None]) in
     interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
       ~impls:newimpls body (lift 1 top_arity)
-- 
cgit v1.2.3