From 6ceaf0176b2a61cd2ed7b358af1e34349a8041ce Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 19 May 2017 21:14:36 +0200
Subject: Moving "sym" on "eq" type to lib/util.ml.

---
 engine/eConstr.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 54d3ce6cf7..0771c83547 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -731,8 +731,6 @@ let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d
 open Context
 open Environ
 
-let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl
-
 let cast_rel_decl :
   type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt =
   fun Refl x -> x
-- 
cgit v1.2.3


From 234dc568769602cb91655929a344027a15f52845 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 19 May 2017 21:19:51 +0200
Subject: In EConstr, defining some "cast" functions earlier.

This allows to use a cast in subst_of_rel_context_instance.

Also added more cast functions for further use.
---
 engine/eConstr.ml | 55 +++++++++++++++++++++++++++++++------------------------
 1 file changed, 31 insertions(+), 24 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 0771c83547..46ac13b695 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -638,6 +638,32 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
+open Context
+open Environ
+
+let cast_list : type a b. (a,b) eq -> a list -> b list =
+  fun Refl x -> x
+
+let cast_list_snd : type a b. (a,b) eq -> ('c * a) list -> ('c * b) list =
+  fun Refl x -> x
+
+let cast_rel_decl :
+  type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt =
+  fun Refl x -> x
+
+let cast_rel_context :
+  type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt =
+  fun Refl x -> x
+
+let cast_named_decl :
+  type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt =
+  fun Refl x -> x
+
+let cast_named_context :
+  type a b. (a,b) eq -> (a, a) Named.pt -> (b, b) Named.pt =
+  fun Refl x -> x
+
+
 module Vars =
 struct
 exception LocalOccur
@@ -647,13 +673,12 @@ let to_constr = unsafe_to_constr
 let lift n c = of_constr (Vars.lift n (to_constr c))
 let liftn n m c = of_constr (Vars.liftn n m (to_constr c))
 
-let substnl subst n c = of_constr (Vars.substnl (List.map to_constr subst) n (to_constr c))
-let substl subst c = of_constr (Vars.substl (List.map to_constr subst) (to_constr c))
+let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (to_constr c))
+let substl subst c = of_constr (Vars.substl (cast_list unsafe_eq subst) (to_constr c))
 let subst1 c r = of_constr (Vars.subst1 (to_constr c) (to_constr r))
 
 let replace_vars subst c =
-  let map (id, c) = (id, to_constr c) in
-  of_constr (Vars.replace_vars (List.map map subst) (to_constr c))
+  of_constr (Vars.replace_vars (cast_list_snd unsafe_eq subst) (to_constr c))
 let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c))
 let subst_vars subst c = of_constr (Vars.subst_vars subst (to_constr c))
 let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
@@ -685,7 +710,8 @@ let closedn sigma n c =
 let closed0 sigma c = closedn sigma 0 c
 
 let subst_of_rel_context_instance ctx subst =
-  List.map of_constr (Vars.subst_of_rel_context_instance (List.map unsafe_to_rel_decl ctx) (List.map to_constr subst))
+  cast_list (sym unsafe_eq)
+    (Vars.subst_of_rel_context_instance (cast_rel_context unsafe_eq ctx) (cast_list unsafe_eq subst))
 
 end
 
@@ -728,25 +754,6 @@ let mkNamedLambda_or_LetIn decl c =
 let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx
 let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx
 
-open Context
-open Environ
-
-let cast_rel_decl :
-  type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt =
-  fun Refl x -> x
-
-let cast_rel_context :
-  type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt =
-  fun Refl x -> x
-
-let cast_named_decl :
-  type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt =
-  fun Refl x -> x
-
-let cast_named_context :
-  type a b. (a,b) eq -> (a, a) Named.pt -> (b, b) Named.pt =
-  fun Refl x -> x
-
 let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e
 let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e
 let push_named d e = push_named (cast_named_decl unsafe_eq d) e
-- 
cgit v1.2.3


From 8bd3e4eba54ace61f49a53b8ce74517de71006ec Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 19 May 2017 21:24:55 +0200
Subject: Exporting some functions of vars.ml as functions operating on
 EConstr.

---
 engine/eConstr.ml  |  7 +++++++
 engine/eConstr.mli | 13 +++++++++++--
 2 files changed, 18 insertions(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 46ac13b695..e5ac3792d6 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -668,6 +668,9 @@ module Vars =
 struct
 exception LocalOccur
 let to_constr = unsafe_to_constr
+let to_rel_decl = unsafe_to_rel_decl
+
+type substl = t list
 
 (** Operations that commute with evar-normalization *)
 let lift n c = of_constr (Vars.lift n (to_constr c))
@@ -677,6 +680,10 @@ let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (t
 let substl subst c = of_constr (Vars.substl (cast_list unsafe_eq subst) (to_constr c))
 let subst1 c r = of_constr (Vars.subst1 (to_constr c) (to_constr r))
 
+let substnl_decl subst n d = of_rel_decl (Vars.substnl_decl (cast_list unsafe_eq subst) n (to_rel_decl d))
+let substl_decl subst d = of_rel_decl (Vars.substl_decl (cast_list unsafe_eq subst) (to_rel_decl d))
+let subst1_decl c d = of_rel_decl (Vars.subst1_decl (to_constr c) (to_rel_decl d))
+
 let replace_vars subst c =
   of_constr (Vars.replace_vars (cast_list_snd unsafe_eq subst) (to_constr c))
 let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c))
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 693b592fd4..9d705b4d55 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -205,12 +205,21 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 module Vars :
 sig
+
+(** See vars.mli for the documentation of the functions below *)
+
+type substl = t list
+
 val lift : int -> t -> t
 val liftn : int -> int -> t -> t
-val substnl : t list -> int -> t -> t
-val substl : t list -> t -> t
+val substnl : substl -> int -> t -> t
+val substl : substl -> t -> t
 val subst1 : t -> t -> t
 
+val substnl_decl : substl -> int -> rel_declaration -> rel_declaration
+val substl_decl : substl -> rel_declaration -> rel_declaration
+val subst1_decl : t -> rel_declaration -> rel_declaration
+
 val replace_vars : (Id.t * t) list -> t -> t
 val substn_vars : int -> Id.t list -> t -> t
 val subst_vars : Id.t list -> t -> t
-- 
cgit v1.2.3