From f7cf2bccd813994e3cd98e97fe9c1c8b5cbde3cf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Feb 2017 23:59:04 +0100
Subject: Better support for printing constructors with let-ins.

This allows e.g. to use the record notations even when there are
defined fields.

A priori fixed also missing parameters when interpreting primitive
tokens.
---
 pretyping/glob_ops.ml  | 33 +++++++++++++++++++++++++++++++++
 pretyping/glob_ops.mli |  2 ++
 2 files changed, 35 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 51660818f4..0eda776519 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -559,12 +559,45 @@ let rec cases_pattern_of_glob_constr na = function
       PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
   | _ -> raise Not_found
 
+open Declarations
+open Term
+open Context
+
+(* Keep only patterns which are not bound to a local definitions *)
+let drop_local_defs typi args =
+    let (decls,_) = decompose_prod_assum typi in
+    let rec aux decls args =
+      match decls, args with
+      | [], [] -> []
+      | Rel.Declaration.LocalDef _ :: decls, pat :: args ->
+         begin
+           match pat with
+           | PatVar (_,Anonymous) -> aux decls args
+           | _ -> raise Not_found (* The pattern is used, one cannot drop it *)
+         end
+      | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
+      | _ -> assert false in
+    aux (List.rev decls) args
+
+let add_patterns_for_params_remove_local_defs (ind,j) l =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let nparams = mib.Declarations.mind_nparams in
+  let l =
+    if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
+      (* Optimisation *) l
+    else
+      let typi = mip.mind_nf_lc.(j-1) in
+      let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in
+      drop_local_defs typi l in
+  Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l
+
 (* Turn a closed cases pattern into a glob_constr *)
 let rec glob_constr_of_closed_cases_pattern_aux = function
   | PatCstr (loc,cstr,[],Anonymous) ->
       GRef (loc,ConstructRef cstr,None)
   | PatCstr (loc,cstr,l,Anonymous) ->
       let ref = GRef (loc,ConstructRef cstr,None) in
+      let l = add_patterns_for_params_remove_local_defs cstr l in
       GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l)
   | _ -> raise Not_found
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 55e6b6533f..6b8f131f41 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -76,3 +76,5 @@ val map_pattern : (glob_constr -> glob_constr) ->
 val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
 
 val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr
+
+val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list
-- 
cgit v1.2.3


From 58e804f07172acc6bb01c8bdafde1217eb4ec4b8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 13 Apr 2017 20:41:40 +0200
Subject: Reinstate fixpoint refolding in [cbn], deactivated by mistake.

Add a test-suite file to be sure we won't regress silently.
---
 pretyping/reductionops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 297f0a1a8e..ba92f64b95 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -755,7 +755,7 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty
     context" in contract_fix *)
 let reduce_and_refold_fix recfun env refold cst_l fix sk =
   let raw_answer =
-    let env = if refold then None else Some env in
+    let env = if refold then Some env else None in
     contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in
   apply_subst
     (fun x (t,sk') ->
-- 
cgit v1.2.3


From 6735a7cbcaa3757e4d9ad60cb5a64fb5197b961e Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 17 May 2017 11:46:31 -0400
Subject: fix swapping of ids in tuples, bug 5486

---
 pretyping/patternops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 75d3ed30ba..79e9c727d7 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -360,9 +360,9 @@ let rec pat_of_raw metas vars = function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (loc,nal,(_,None),b,c) ->
-      let mkGLambda c na =
+      let mkGLambda na c =
 	GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in
-      let c = List.fold_left mkGLambda c nal in
+      let c = List.fold_right mkGLambda nal c in
       let cip =
 	{ cip_style = LetStyle;
 	  cip_ind = None;
-- 
cgit v1.2.3