Merge PR#707: add support for "-bypass-API" argument to "coq_makefile"

4 files changed, 38 insertions, 3 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e53d19b595..62ff9ac708 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -457,11 +457,44 @@ let rec cases_pattern_of_glob_constr na = CAst.map (function
   | _ -> 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.CAst.v 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 (CAst.make @@ PatVar Anonymous) l
+
 (* Turn a closed cases pattern into a glob_constr *)
 let rec glob_constr_of_closed_cases_pattern_aux x = CAst.map_with_loc (fun ?loc -> function
   | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
   | PatCstr (cstr,l,Anonymous)  ->
       let ref = CAst.make ?loc @@ GRef (ConstructRef cstr,None) in
+      let l = add_patterns_for_params_remove_local_defs cstr l in
       GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
   | _ -> raise Not_found
   ) x
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index f7cc08ca21..75db04f77f 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -81,3 +81,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
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index db2e5da957..c36542aebc 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -364,9 +364,9 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
-      let mkGLambda c na = CAst.make ?loc @@
+      let mkGLambda na c = CAst.make ?loc @@
 	GLambda (na,Explicit, CAst.make @@ GHole (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;
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b4654bfb56..52d1ffe06d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -777,7 +777,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
     context" in contract_fix *)
 let reduce_and_refold_fix recfun env sigma 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 sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
   apply_subst
     (fun sigma x (t,sk') ->