From 6b9a9124d3bd24fe9305df613547139f6f609c60 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Aug 2017 16:15:57 +0200
Subject: Moving the argument of CProdN/CLambdaN from binder_expr to
 local_binder_expr.

The motivations are:

- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
  before this patch, there is a different treatment of `Definition f
  '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
  to interpret `Definition f `pat := c : t`. With the patch, the fix
  to avoid seeing a variable named `pat` works for both `fun 'x =>
  ...` and `Definition f 'x := ...`.

The drawbacks are:

- Counterpart to reflecting the concrete syntax more closerly, there
  are more redundancies in the syntax. For instance, the case `CLetIn
  (na,b,t,c)` can appears also in the form `CProdN (CLocalDef
  (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
---
 plugins/ltac/g_tactic.ml4 | 6 ++++--
 plugins/ltac/pptactic.ml  | 7 ++++---
 2 files changed, 8 insertions(+), 5 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index d792d4ff7d..e68140828a 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -115,10 +115,11 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
     match bl,ann with
         [([_],_,_)], None -> 1
       | _, Some x ->
-          let ids = List.map snd (List.flatten (List.map pi1 bl)) in
+          let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in
           (try List.index Names.Name.equal (snd x) ids
           with Not_found -> user_err Pp.(str "No such fix variable."))
       | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in
+  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
   (id,n, CAst.make ~loc @@ CProdN(bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
@@ -126,6 +127,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
     user_err ~loc:aloc
       ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
+  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
   (id,CAst.make ~loc @@ CProdN(bl,ty))
 
 (* Functions overloaded by quotifier *)
@@ -160,7 +162,7 @@ let mkTacCase with_evar = function
 let rec mkCLambdaN_simple_loc ?loc bll c =
   match bll with
   | ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
+      CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
   | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c
   | [] -> c
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e5ff473568..4f430b79e4 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -353,9 +353,10 @@ let string_of_genarg_arg (ArgumentType arg) =
     let rec strip_ty acc n ty =
       match ty.CAst.v with
           Constrexpr.CProdN(bll,a) ->
-            let nb =
-              List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
-            let bll = List.map (fun (x, _, y) -> x, y) bll in
+            let bll = List.map (function
+            | CLocalAssum (nal,_,t) -> nal,t
+            | _ -> user_err Pp.(str "Cannot translate fix tactic: not only products")) bll in
+            let nb = List.fold_left (fun i (nal,t) -> i + List.length nal) 0 bll in
             if nb >= n then (List.rev (bll@acc)), a
             else strip_ty (bll@acc) (n-nb) a
         | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
-- 
cgit v1.2.3


From 69822345c198aa6bf51354f6b84c7fd5d401bc9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 23 Aug 2017 20:32:15 +0200
Subject: Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.

Renaming it register_grammars_by_name.
---
 plugins/ltac/tacentries.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index ee84be5414..8112cc4008 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -545,11 +545,10 @@ let print_located_tactic qid =
 (** Grammar *)
 
 let () =
-  let open Metasyntax in
   let entries = [
     AnyEntry Pltac.tactic_expr;
     AnyEntry Pltac.binder_tactic;
     AnyEntry Pltac.simple_tactic;
     AnyEntry Pltac.tactic_arg;
   ] in
-  register_grammar "tactic" entries
+  register_grammars_by_name "tactic" entries
-- 
cgit v1.2.3