Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

1 files changed, 21 insertions, 20 deletions

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index cb08b5058f..91b40be7e9 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -277,7 +277,7 @@ and reduce_lapp substf lids body substa largs =
   | [], _::_ -> simplify_app substf body substa (Array.of_list largs)
 
 
-(* [occurence kind k lam]:
+(* [occurrence kind k lam]:
    If [kind] is [true] return [true] if the variable [k] does not appear in 
    [lam], return [false] if the variable appear one time and not
    under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
@@ -285,7 +285,7 @@ and reduce_lapp substf lids body substa largs =
    else raise [Not_found]
 *)
 
-let rec occurence k kind lam =   
+let rec occurrence k kind lam =
   match lam with
   | Lrel (_,n) -> 
       if Int.equal n k then 
@@ -294,35 +294,35 @@ let rec occurence k kind lam =
   | Lvar _  | Lconst _  | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _
   | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
   | Lprod(dom, codom) ->
-      occurence k (occurence k kind dom) codom
+      occurrence k (occurrence k kind dom) codom
   | Llam(ids,body) ->
-      let _ = occurence (k+Array.length ids) false body in kind
+      let _ = occurrence (k+Array.length ids) false body in kind
   | Llet(_,def,body) ->
-      occurence (k+1) (occurence k kind def) body
+      occurrence (k+1) (occurrence k kind def) body
   | Lapp(f, args) ->
-      occurence_args k (occurence k kind f) args
+      occurrence_args k (occurrence k kind f) args
   | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) ->
-      occurence_args k kind args
+      occurrence_args k kind args
   | Lcase(_,t,a,br) ->
-      let kind = occurence k (occurence k kind t) a in
+      let kind = occurrence k (occurrence k kind t) a in
       let r = ref kind in
       Array.iter (fun (_,ids,c) -> 
-	r := occurence (k+Array.length ids) kind c && !r) br;
+	r := occurrence (k+Array.length ids) kind c && !r) br;
       !r 
   | Lif (t, bt, bf) ->
-      let kind = occurence k kind t in
-      kind && occurence k kind bt && occurence k kind bf
+      let kind = occurrence k kind t in
+      kind && occurrence k kind bt && occurrence k kind bf
   | Lfix(_,(ids,ltypes,lbodies)) 
   | Lcofix(_,(ids,ltypes,lbodies)) ->
-      let kind = occurence_args k kind ltypes in
-      let _ = occurence_args (k+Array.length ids) false lbodies in
+      let kind = occurrence_args k kind ltypes in
+      let _ = occurrence_args (k+Array.length ids) false lbodies in
       kind 
 
-and occurence_args k kind args = 
-  Array.fold_left (occurence k) kind args
+and occurrence_args k kind args =
+  Array.fold_left (occurrence k) kind args
     
 let occur_once lam = 
-  try let _ = occurence 1 true lam in true
+  try let _ = occurrence 1 true lam in true
   with Not_found -> false
       
 (* [remove_let lam] remove let expression in [lam] if the variable is *)
@@ -379,7 +379,7 @@ let rec get_alias env (kn, u as p) =
     | None -> p
     | Some tps ->
        match Cemitcodes.force tps with
-       | Cemitcodes.BCalias kn' -> get_alias env kn'
+       | Cemitcodes.BCalias kn' -> get_alias env (kn', u)
        | _ -> p
 
 (*i Global environment *)
@@ -485,7 +485,7 @@ module Renv =
     let pop env = Vect.pop env.name_rel
 	    
     let popn env n =
-      for i = 1 to n do pop env done
+      for _i = 1 to n do pop env done
 
     let get env n =
       Lrel (Vect.get_last env.name_rel (n-1), n)
@@ -727,7 +727,8 @@ let optimize lam =
 let lambda_of_constr env sigma c =
   set_global_env env;
   let env = Renv.make () in
-  let ids = List.rev_map (fun (id, _, _) -> id) !global_env.env_rel_context in
+  let open Context.Rel.Declaration in
+  let ids = List.rev_map get_name !global_env.env_rel_context in
   Renv.push_rels env (Array.of_list ids);
   let lam = lambda_of_constr env sigma c in
 (*  if Flags.vm_draw_opt () then begin