From be11ab322fa73804118738e7a08e9910fdf4600d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 22 Oct 2016 11:03:13 +0200
Subject: Renamings to avoid confusion deprecating old names

reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
---
 plugins/ssrmatching/ssrmatching.ml4 | 2 +-
 plugins/ssrmatching/ssrmatching.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index a34fa4cae7..88f028b4b7 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -355,7 +355,7 @@ let nf_open_term sigma0 ise c =
   !s', Evd.evar_universe_context s, c'
 
 let unif_end env sigma0 ise0 pt ok =
-  let ise = Evarconv.consider_remaining_unif_problems env ise0 in
+  let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
   let s, uc, t = nf_open_term sigma0 ise pt in
   let ise1 = create_evar_defs s in
   let ise1 = Evd.set_universe_context ise1 uc in
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 74a603e51c..288a04e60a 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -213,7 +213,7 @@ val assert_done : 'a option ref -> 'a
 
 (** Very low level APIs.
     these are calls to evarconv's [the_conv_x] followed by
-    [consider_remaining_unif_problems] and [resolve_typeclasses].
+    [solve_unif_constraints_with_heuristics] and [resolve_typeclasses].
     In case of failure they raise [NoMatch] *)
 
 val unify_HO : env -> evar_map -> constr -> constr -> evar_map
-- 
cgit v1.2.3


From b16de62d20790930589795c3d10fbb07185ec22c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 24 Nov 2016 14:02:41 +0100
Subject: Lazily load constants in micromega (bug #5134).

---
 plugins/micromega/coq_micromega.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a063cbbfe3..e4b58a56f9 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1517,27 +1517,27 @@ let rec apply_ids t ids =
   | [] -> t
   | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
 
-let coq_Node = 
+let coq_Node = lazy
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
-let coq_Leaf = 
+let coq_Leaf = lazy
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")
-let coq_Empty = 
+let coq_Empty = lazy
  (Coqlib.gen_constant_in_modules "VarMap"
    [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
 
-let coq_VarMap = 
+let coq_VarMap = lazy
   (Coqlib.gen_constant_in_modules "VarMap"
      [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")
  
 
 let rec dump_varmap typ m =
   match m with
-  | Mc.Empty -> Term.mkApp(coq_Empty,[| typ |])
-  | Mc.Leaf v -> Term.mkApp(coq_Leaf,[| typ; v|])
-  | Mc.Node(l,o,r) -> 
-    Term.mkApp (coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
+  | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |])
+  | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|])
+  | Mc.Node(l,o,r) ->
+    Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
 
 
 let vm_of_list env =
@@ -1709,7 +1709,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
     (set
       [
        ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
-       ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|])); 
+       ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
        ("__wit", cert, cert_typ)
       ]
       (Tacmach.pf_concl gl))
-- 
cgit v1.2.3


From a4db30e1cd6c21a466549835a86d61f95db36c82 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Apr 2016 22:24:59 +0200
Subject: Fixing printers for pr_auto_using and pr_firstorder_using.

---
 plugins/firstorder/g_ground.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 95095b09cb..43fac8ad83 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -116,9 +116,9 @@ open Pp
 open Genarg
 open Ppconstr
 open Printer
-let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l
-let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
-let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
 
 let warn_deprecated_syntax =
   CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
-- 
cgit v1.2.3


From 436782a98f9f8d452f9b60cb27cd90a7bcf33253 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 5 Dec 2016 13:29:17 +0100
Subject: ssrmatching: handle primite projections (fix: #5247)

---
 plugins/ssrmatching/ssrmatching.ml4 | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index ef04bef8e6..11f45d5d86 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -434,7 +434,7 @@ let proj_nparams c =
   try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
 
 let isFixed c = match kind_of_term c with
-  | Var _ | Ind _ | Construct _ | Const _ -> true
+  | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true
   | _ -> false
 
 let isRigid c = match kind_of_term c with
@@ -486,6 +486,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
       let np = proj_nparams p in
       if np = 0 || np > List.length a then KpatConst, f, a else
       let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2
+    | Proj (p,arg) -> KpatProj (Projection.constant p), f, a
     | Var _ | Ind _ | Construct _ -> KpatFixed, f, a
     | Evar (k, _) ->
       if Evd.mem sigma0 k then KpatEvar k, f, a else
@@ -566,6 +567,10 @@ let filter_upat i0 f n u fpats =
   if np < na then fpats else
   let () = if !i0 < np then i0 := n in (u, np) :: fpats
 
+let eq_prim_proj c t = match kind_of_term t with
+  | Proj(p,_) -> Constant.equal (Projection.constant p) c
+  | _ -> false
+
 let filter_upat_FO i0 f n u fpats =
   let np = nb_args u.up_FO in
   if n < np then fpats else
@@ -576,7 +581,7 @@ let filter_upat_FO i0 f n u fpats =
   | KpatLet -> isLetIn f
   | KpatLam -> isLambda f
   | KpatRigid -> isRigid f
-  | KpatProj pc -> Term.eq_constr f (mkConst pc)
+  | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f
   | KpatFlex -> i0 := n; true in
   if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats
 
-- 
cgit v1.2.3


From 80bd0e81305abfc76831ff1c8361e01c4aabb68e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 7 Dec 2016 12:34:35 +0100
Subject: ssrmatching: fix iter_constr_LR iterator wrt Proj

---
 plugins/ssrmatching/ssrmatching.ml4 | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 11f45d5d86..d21223d43d 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -390,7 +390,8 @@ let iter_constr_LR f c = match kind_of_term c with
   | Case (_, p, v, b) -> f v; f p; Array.iter f b
   | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
     for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
-  | _ -> ()
+  | Proj(_,a) -> f a
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _) -> ()
 
 (* The comparison used to determine which subterms matches is KEYED        *)
 (* CONVERSION. This looks for convertible terms that either have the same  *)
@@ -524,7 +525,13 @@ let nb_cs_proj_args pc f u =
   try match kind_of_term f with
   | Prod _ -> na Prod_cs
   | Sort s -> na (Sort_cs (family_of_sort s))
-  | Const (c',_) when Constant.equal c' pc -> Array.length (snd (destApp u.up_f))
+  | Const (c',_) when Constant.equal c' pc ->
+      begin match kind_of_term u.up_f with
+      | App(_,args) -> Array.length args
+      | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
+                       the number of arguments including the projected *)
+      | _ -> assert false
+      end
   | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f))
   | _ -> -1
   with Not_found -> -1
-- 
cgit v1.2.3


From 90b61424761c5ba1ddbecf20c29d78b485584ae7 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Mon, 12 Dec 2016 14:18:48 +0100
Subject: Extend Fast_typeops to be a replacement for Typeops

This brings the fix in cad44fc for #2996 to the copy of
Fast_typeops.check_hyps_inclusion.

Fast_typeops.constant_type checks the universe constraints instead of
outputting them. Since everyone who used Typeops.constant_type just
discarded the constraints they've been switched to constant_type_in
which should be the same in Fast_typeops and Typeops.

There are some small differences in the interfaces:
- Typeops.type_of_projection <->
  Fast_typeops.type_of_projection_constant to avoid collision with the
  internally used type_of_projection (which gives the type of [Proj(p,c)]).
- check_hyps_inclusion takes [('a -> constr)] and ['a] instead of
  [constr] for reporting errors.
---
 plugins/cc/ccalgo.ml             | 2 +-
 plugins/extraction/extraction.ml | 2 +-
 plugins/funind/recdef.ml         | 8 +++++---
 3 files changed, 7 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc53b113df..7347c3c2cd 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -444,7 +444,7 @@ and applist_projection c l =
     let p = Projection.make (fst c) false in
     (match l with 
     | [] -> (* Expand the projection *)
-      let ty,_ = Typeops.type_of_constant (Global.env ()) c in
+      let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *)
       let pb = Environ.lookup_projection p (Global.env()) in
       let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
 	it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a980a43f53..33fab74e13 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -258,7 +258,7 @@ let rec extract_type env db j c args =
     | Const (kn,u as c) ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
-	let typ,_ = Typeops.type_of_constant env c in
+        let typ = Typeops.type_of_constant_in env c in (* FIXME constraints *)
 	(match flag_of_type env typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 54066edfb8..e00fa528ad 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -78,8 +78,10 @@ let def_of_const t =
 
 let type_of_const t =
    match (kind_of_term t) with
-    Const sp -> Typeops.type_of_constant (Global.env()) sp
-    |_ -> assert false
+   | Const sp ->
+      (* FIXME discarding universe constraints *)
+      Typeops.type_of_constant_in (Global.env()) sp
+   |_ -> assert false
 
 let constr_of_global x = 
   fst (Universes.unsafe_constr_of_global x)
@@ -1422,7 +1424,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
   (cont_tactic:Id.t list -> tactic) g =
   let ids = pf_ids_of_hyps g in
   let terminate_constr = constr_of_global term_f in
-  let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in
+  let nargs = nb_prod (type_of_const terminate_constr) in
   let x = n_x_id ids nargs in
   observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
     h_intros x;
-- 
cgit v1.2.3


From 90b6969c467f097a4d7da0140e1351ef98d6401d Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 28 Jan 2017 14:11:50 +0100
Subject: Remove useless comments

---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 33fab74e13..2b19c2805f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -258,7 +258,7 @@ let rec extract_type env db j c args =
     | Const (kn,u as c) ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
-        let typ = Typeops.type_of_constant_in env c in (* FIXME constraints *)
+        let typ = Typeops.type_of_constant_in env c in
 	(match flag_of_type env typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
-- 
cgit v1.2.3


From 5484ba750ef4526dde29ffc1474ca5d145f3ec04 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 4 Feb 2017 01:01:05 +0100
Subject: Extraction: fix complexity issue #5310

  A double call to pp_module_type inside Ocaml.pp_specif was
  causing an complexity blowup when pretty-printing heavily modular
  extracted code.

  I wasn't able to figure out why this double call is there. It could
  be the leftover of some intermediate work in 2007 before commit 350398eae
  (which introduced global printing phases Pre/Impl/Intf).

  Anyway I'm reasonably sure that today these two pp_module_type calls produce
  the exact same pretty-printed signature (even if there's a large bunch of
  imperative states around). Moreover, this duplicated signature is actually
  slightly wrong: when we alias a module M with a unambiguous name like Coq__123,
  the type of Coq__123 should not be an exact copy of the type of M, but rather
  a "strengthened" version of it (with equality between inductive types).
  So the best solution is now to use this funny feature of OCaml introduced in 3.12 :

  module Coq__123 : module type of struct include M end

  This "module type of struct include" is slightly awkward, but short, correct,
  and trivial to produce :-). And I doubt anybody will object to the (rare) use
  of some 3.12 features in extracted code of 2017...
---
 plugins/extraction/ocaml.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 1c29a9bc24..5d10cb939d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -618,12 +618,13 @@ let rec pp_specif = function
        with Not_found -> pp_spec s)
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
-      let def' = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
       (try
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def')
+         fnl () ++
+         hov 1 (str ("module "^ren^" :") ++ spc () ++
+                str "module type of struct include " ++ name ++ str " end")
        with Not_found -> Pp.mt ())
   | (l,Smodtype mt) ->
       let def = pp_module_type [] mt in
-- 
cgit v1.2.3


From af4962a9211a707943e7b0627439a731c3e7d23f Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 4 Feb 2017 19:29:15 +0100
Subject: Extraction : get_duplicates (via option) instead of check_duplicates
 (via Not_found)

 This clarifies the execution flow
---
 plugins/extraction/common.ml  | 16 ++++++++-------
 plugins/extraction/common.mli |  2 +-
 plugins/extraction/ocaml.ml   | 45 ++++++++++++++++++++-----------------------
 3 files changed, 31 insertions(+), 32 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9446cf667c..de97ba97c3 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -308,15 +308,16 @@ end
 
 module DupMap = Map.Make(DupOrd)
 
-let add_duplicate, check_duplicate =
+let add_duplicate, get_duplicate =
   let index = ref 0 and dups = ref DupMap.empty in
   register_cleanup (fun () -> index := 0; dups := DupMap.empty);
   let add mp l =
      incr index;
      let ren = "Coq__" ^ string_of_int !index in
      dups := DupMap.add (mp,l) ren !dups
-  and check mp l = DupMap.find (mp, l) !dups
-  in (add,check)
+  and get mp l =
+    try Some (DupMap.find (mp, l) !dups) with Not_found -> None
+  in (add,get)
 
 type reset_kind = AllButExternal | Everything
 
@@ -510,10 +511,11 @@ let pp_duplicate k' prefix mp rls olab =
       (* Here rls=s::rls', we search the label for s inside mp *)
       List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp
   in
-  try dottify (check_duplicate prefix lbl :: rls')
-  with Not_found ->
-    assert (get_phase () == Pre); (* otherwise it's too late *)
-    add_duplicate prefix lbl; dottify rls
+  match get_duplicate prefix lbl with
+  | Some ren -> dottify (ren :: rls')
+  | None ->
+     assert (get_phase () == Pre); (* otherwise it's too late *)
+     add_duplicate prefix lbl; dottify rls
 
 let fstlev_ks k = function
   | [] -> assert false
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 2f5601964e..b8e95afb38 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -62,7 +62,7 @@ val top_visible_mp : unit -> module_path
 val push_visible : module_path -> module_path list -> unit
 val pop_visible : unit -> unit
 
-val check_duplicate : module_path -> Label.t -> string
+val get_duplicate : module_path -> Label.t -> string option
 
 type reset_kind = AllButExternal | Everything
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 5d10cb939d..31e481d123 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -610,30 +610,29 @@ let pp_alias_spec ren = function
 let rec pp_specif = function
   | (_,Spec (Sval _ as s)) -> pp_spec s
   | (l,Spec s) ->
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+     (match Common.get_duplicate (top_visible_mp ()) l with
+      | None -> pp_spec s
+      | Some ren ->
 	 hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
 	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_spec ren s
-       with Not_found -> pp_spec s)
+	 pp_alias_spec ren s)
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> Pp.mt ()
+       | Some ren ->
          fnl () ++
          hov 1 (str ("module "^ren^" :") ++ spc () ++
-                str "module type of struct include " ++ name ++ str " end")
-       with Not_found -> Pp.mt ())
+                str "module type of struct include " ++ name ++ str " end"))
   | (l,Smodtype mt) ->
       let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> Pp.mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> Pp.mt ()
+       | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
 
 and pp_module_type params = function
   | MTident kn ->
@@ -682,12 +681,12 @@ let is_short = function MEident _ | MEapply _ -> true | _ -> false
 
 let rec pp_structure_elem = function
   | (l,SEdecl d) ->
-       (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+     (match Common.get_duplicate (top_visible_mp ()) l with
+      | None -> pp_decl d
+      | Some ren ->
 	 hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
 	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_decl ren d
-	with Not_found -> pp_decl d)
+	 pp_alias_decl ren d)
   | (l,SEmodule m) ->
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
@@ -700,18 +699,16 @@ let rec pp_structure_elem = function
       hov 1
 	(str "module " ++ name ++ typ ++ str " =" ++
 	 (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ str ("module "^ren^" = ") ++ name
-       with Not_found -> mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name
+       | None -> mt ())
   | (l,SEmodtype m) ->
       let def = pp_module_type [] m in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-         fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> mt ()
+       | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
 
 and pp_module_expr params = function
   | MEident mp -> pp_modname mp
-- 
cgit v1.2.3


From 8ef3bc0e8a65b3a0338da39aa54cd75b1c2c1bb7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 4 Feb 2017 19:55:18 +0100
Subject: Extraction: simplify the generated code for difficult name conflicts

 No more pp_alias_spec et pp_alias_decl.
 Instead, we use "include" and "module type of".
 The extracted code might hence need OCaml 3.12 (quite rarely)
---
 plugins/extraction/ocaml.ml | 33 ++-------------------------------
 1 file changed, 2 insertions(+), 31 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 31e481d123..404939cff9 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -555,24 +555,6 @@ let pp_decl = function
     | Dfix (rv,defs,typs) ->
 	pp_Dfix (rv,defs,typs)
 
-let pp_alias_decl ren = function
-  | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Dtype (r, l, _) ->
-      let name = pp_global Type r in
-      let l = rename_tvars keywords l in
-      let ids = pp_parameters l in
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
-	     str (ren^".") ++ name)
-  | Dterm (r, a, t) ->
-      let name = pp_global Term r in
-      hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
-  | Dfix (rv, _, _) ->
-      prvecti (fun i r -> if is_inline_custom r then mt () else
-		 let name = pp_global Term r in
-		 hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
-		 fnl ())
-	rv
-
 let pp_spec = function
   | Sval (r,_) when is_inline_custom r -> mt ()
   | Stype (r,_,_) when is_inline_custom r -> mt ()
@@ -597,16 +579,6 @@ let pp_spec = function
       in
       hov 2 (str "type " ++ ids ++ name ++ def)
 
-let pp_alias_spec ren = function
-  | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Stype (r,l,_) ->
-      let name = pp_global Type r in
-      let l = rename_tvars keywords l in
-      let ids = pp_parameters l in
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
-	     str (ren^".") ++ name)
-  | Sval _ -> assert false
-
 let rec pp_specif = function
   | (_,Spec (Sval _ as s)) -> pp_spec s
   | (l,Spec s) ->
@@ -615,7 +587,7 @@ let rec pp_specif = function
       | Some ren ->
 	 hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
 	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_spec ren s)
+         str ("include module type of struct include "^ren^" end"))
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
@@ -685,8 +657,7 @@ let rec pp_structure_elem = function
       | None -> pp_decl d
       | Some ren ->
 	 hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
-	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_decl ren d)
+	 fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
   | (l,SEmodule m) ->
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
-- 
cgit v1.2.3


From 69c4e7cfa0271f024b2178082e4be2e3ca3be263 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 5 Feb 2017 01:46:41 +0100
Subject: Extraction: avoid deprecated functions of module String

 - A few tweaks of string are now done via the Bytes module
 - lots of String.capitalize_ascii and co
---
 plugins/extraction/common.ml  | 13 ++++++++-----
 plugins/extraction/common.mli |  3 +++
 plugins/extraction/haskell.ml |  4 ++--
 plugins/extraction/scheme.ml  |  7 +------
 plugins/extraction/table.ml   | 11 ++++++-----
 5 files changed, 20 insertions(+), 18 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index de97ba97c3..b93a76b966 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -92,9 +92,11 @@ let begins_with_CoqXX s =
 let unquote s =
   if lang () != Scheme then s
   else
-    let s = String.copy s in
-    for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done;
-    s
+    let b = Bytes.of_string s in
+    for i=0 to Bytes.length b - 1 do
+      if Bytes.get b i == '\'' then Bytes.set b i '~'
+    done;
+    Bytes.to_string b
 
 let rec qualify delim = function
   | [] -> assert false
@@ -110,12 +112,13 @@ let pseudo_qualify = qualify "__"
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
-let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id))
+let lowercase_id id =
+  Id.of_string (String.uncapitalize_ascii (ascii_of_id id))
 let uppercase_id id =
   let s = ascii_of_id id in
   assert (not (String.is_empty s));
   if s.[0] == '_' then Id.of_string ("Coq_"^s)
-  else Id.of_string (String.capitalize s)
+  else Id.of_string (String.capitalize_ascii s)
 
 type kind = Term | Type | Cons | Mod
 
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index b8e95afb38..a6351fc4c4 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -36,6 +36,9 @@ val pr_binding : Id.t list -> std_ppcmds
 
 val rename_id : Id.t -> Id.Set.t -> Id.t
 
+(** For Scheme extraction, replace the ['] by [~] *)
+val unquote : string -> string
+
 type env = Id.t list * Id.Set.t
 val empty_env : unit -> env
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 0692c88cd1..83bb2e135e 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -21,8 +21,8 @@ open Common
 
 (*s Haskell renaming issues. *)
 
-let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
-let pr_upper_id id = str (String.capitalize (Id.to_string id))
+let pr_lower_id id = str (String.uncapitalize_ascii (Id.to_string id))
+let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id))
 
 let keywords =
   List.fold_right (fun s -> Id.Set.add (Id.of_string s))
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index a6309e61f9..3bd16138f9 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -39,12 +39,7 @@ let preamble _ comment _ usf =
   str "(load \"macros_extr.scm\")\n\n" ++
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
-let pr_id id =
-  let s = Id.to_string id in
-  for i = 0 to String.length s - 1 do
-    if s.[i] == '\'' then s.[i] <- '~'
-  done;
-  str s
+let pr_id id = str (unquote (Id.to_string id))
 
 let paren = pp_par true
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 5e7d810c93..a8d49ffda5 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -55,7 +55,7 @@ let is_modfile = function
   | _ -> false
 
 let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f)))
+  | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f)))
   | _ -> assert false
 
 let is_toplevel mp =
@@ -773,13 +773,14 @@ let file_of_modfile mp =
     | MPfile f -> Id.to_string (List.hd (DirPath.repr f))
     | _ -> assert false
   in
-  let s = String.copy (string_of_modfile mp) in
-  if s.[0] != s0.[0] then s.[0] <- s0.[0];
-  s
+  let s = Bytes.of_string (string_of_modfile mp) in
+  let () = Bytes.set s 0 (s0.[0]) in
+  Bytes.to_string s
 
 let add_blacklist_entries l =
   blacklist_table :=
-    List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s)))
+    List.fold_right
+      (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s)))
       l !blacklist_table
 
 (* Registration of operations for rollback. *)
-- 
cgit v1.2.3


From 093ce7c6a03e6e48c9b8f20a810d553fb953fe72 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 5 Feb 2017 02:01:56 +0100
Subject: Extraction: remove the "print to devnull" hack now that pp isn't lazy
 anymore

---
 plugins/extraction/extract_env.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 52f22ee603..e019bb3c2a 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -507,8 +507,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
   in
   (* First, a dry run, for computing objects to rename or duplicate *)
   set_phase Pre;
-  let devnull = formatter true None in
-  pp_with devnull (d.pp_struct struc);
+  ignore (d.pp_struct struc);
   let opened = opened_libraries () in
   (* Print the implementation *)
   let cout = if dry then None else Option.map open_out fn in
-- 
cgit v1.2.3


From df14dac0e6e9d9819dcc3b1601e150af7c142597 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 5 Feb 2017 02:12:36 +0100
Subject: Extraction cosmetic: no whitespaces in printing empty modules

---
 plugins/extraction/ocaml.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 404939cff9..d89bf95ee8 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -625,8 +625,10 @@ and pp_module_type params = function
       let l = List.rev l in
       pop_visible ();
       str "sig" ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
-	fnl () ++ str "end"
+      (if List.is_empty l then mt ()
+       else
+         v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+      ++ str "end"
   | MTwith(mt,ML_With_type(idl,vl,typ)) ->
       let ids = pp_parameters (rename_tvars keywords vl) in
       let mp_mt = msid_of_mt mt in
@@ -701,8 +703,10 @@ and pp_module_expr params = function
       let l = List.rev l in
       pop_visible ();
       str "struct" ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
-      fnl () ++ str "end"
+      (if List.is_empty l then mt ()
+       else
+         v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+      ++ str "end"
 
 let rec prlist_sep_nonempty sep f = function
   | [] -> mt ()
-- 
cgit v1.2.3


From 3550120641c3b8d84290dc950e717aaf099775f9 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 7 Feb 2017 23:28:36 +0100
Subject: Revert "Extraction: avoid deprecated functions of module String"

This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263.

String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
---
 plugins/extraction/common.ml  | 13 +++++--------
 plugins/extraction/common.mli |  3 ---
 plugins/extraction/haskell.ml |  4 ++--
 plugins/extraction/scheme.ml  |  7 ++++++-
 plugins/extraction/table.ml   | 11 +++++------
 5 files changed, 18 insertions(+), 20 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index b93a76b966..de97ba97c3 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -92,11 +92,9 @@ let begins_with_CoqXX s =
 let unquote s =
   if lang () != Scheme then s
   else
-    let b = Bytes.of_string s in
-    for i=0 to Bytes.length b - 1 do
-      if Bytes.get b i == '\'' then Bytes.set b i '~'
-    done;
-    Bytes.to_string b
+    let s = String.copy s in
+    for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done;
+    s
 
 let rec qualify delim = function
   | [] -> assert false
@@ -112,13 +110,12 @@ let pseudo_qualify = qualify "__"
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
-let lowercase_id id =
-  Id.of_string (String.uncapitalize_ascii (ascii_of_id id))
+let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id))
 let uppercase_id id =
   let s = ascii_of_id id in
   assert (not (String.is_empty s));
   if s.[0] == '_' then Id.of_string ("Coq_"^s)
-  else Id.of_string (String.capitalize_ascii s)
+  else Id.of_string (String.capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index a6351fc4c4..b8e95afb38 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -36,9 +36,6 @@ val pr_binding : Id.t list -> std_ppcmds
 
 val rename_id : Id.t -> Id.Set.t -> Id.t
 
-(** For Scheme extraction, replace the ['] by [~] *)
-val unquote : string -> string
-
 type env = Id.t list * Id.Set.t
 val empty_env : unit -> env
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 83bb2e135e..0692c88cd1 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -21,8 +21,8 @@ open Common
 
 (*s Haskell renaming issues. *)
 
-let pr_lower_id id = str (String.uncapitalize_ascii (Id.to_string id))
-let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id))
+let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
+let pr_upper_id id = str (String.capitalize (Id.to_string id))
 
 let keywords =
   List.fold_right (fun s -> Id.Set.add (Id.of_string s))
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 3bd16138f9..a6309e61f9 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -39,7 +39,12 @@ let preamble _ comment _ usf =
   str "(load \"macros_extr.scm\")\n\n" ++
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
-let pr_id id = str (unquote (Id.to_string id))
+let pr_id id =
+  let s = Id.to_string id in
+  for i = 0 to String.length s - 1 do
+    if s.[i] == '\'' then s.[i] <- '~'
+  done;
+  str s
 
 let paren = pp_par true
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a8d49ffda5..5e7d810c93 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -55,7 +55,7 @@ let is_modfile = function
   | _ -> false
 
 let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f)))
+  | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f)))
   | _ -> assert false
 
 let is_toplevel mp =
@@ -773,14 +773,13 @@ let file_of_modfile mp =
     | MPfile f -> Id.to_string (List.hd (DirPath.repr f))
     | _ -> assert false
   in
-  let s = Bytes.of_string (string_of_modfile mp) in
-  let () = Bytes.set s 0 (s0.[0]) in
-  Bytes.to_string s
+  let s = String.copy (string_of_modfile mp) in
+  if s.[0] != s0.[0] then s.[0] <- s0.[0];
+  s
 
 let add_blacklist_entries l =
   blacklist_table :=
-    List.fold_right
-      (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s)))
+    List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s)))
       l !blacklist_table
 
 (* Registration of operations for rollback. *)
-- 
cgit v1.2.3