1 files changed, 25 insertions, 29 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index f5f6a3eb..828d652c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Globnames
@@ -68,15 +68,14 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
 let is_contextual_implicit_args () = !implicit_args.contextual
 let is_maximal_implicit_args () = !implicit_args.maximal
 
-let with_implicits flags f x =
+let with_implicit_protection f x =
   let oflags = !implicit_args in
   try
-    implicit_args := flags;
     let rslt = f x in
     implicit_args := oflags;
     rslt
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     let () = implicit_args := oflags in
     iraise reraise
 
@@ -165,6 +164,7 @@ let update pos rig (na,st) =
 
 (* modified is_rigid_reference with a truncated env *)
 let is_flexible_reference env bound depth f =
+  let open Context.Named.Declaration in
   match kind_of_term f with
     | Rel n when n >= bound+depth -> (* inductive type *) false
     | Rel n when n >= depth -> (* previous argument *) true
@@ -173,8 +173,7 @@ let is_flexible_reference env bound depth f =
         let cb = Environ.lookup_constant kn env in
 	(match cb.const_body with Def _ -> true | _ -> false)
     | Var id ->
-        let (_, value, _) = Environ.lookup_named id env in
-        begin match value with None -> false | _ -> true end
+        Environ.lookup_named id env |> is_local_def
     | Ind _ | Construct _ -> false
     |  _ -> true
 
@@ -188,7 +187,7 @@ let is_reversible_pattern bound depth f l =
 (* Precondition: rels in env are for inductive types only *)
 let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
   let rec frec rig (env,depth as ed) c =
-    let hd = if strict then whd_betadeltaiota env c else c in
+    let hd = if strict then whd_all env c else c in
     let c = if strongly_strict then hd else c in
     match kind_of_term hd with
     | Rel n when (n < bound+depth) && (n >= depth) ->
@@ -234,13 +233,14 @@ let find_displayed_name_in all avoid na (_,b as envnames_b) =
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
+  let open Context.Rel.Declaration in
   let rec aux env avoid n names t =
-    let t = whd_betadeltaiota env t in
+    let t = whd_all env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
 	  let na',avoid' = find_displayed_name_in all avoid na (names,b) in
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
-            (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
+            (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b)
       | _ ->
 	  rigid := is_rigid_head t;
 	  let names = List.rev names in
@@ -249,10 +249,10 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
 	    add_free_rels_until strict strongly_strict revpat n env t Conclusion v
 	  else v
   in
-  match kind_of_term (whd_betadeltaiota env t) with
+  match kind_of_term (whd_all env t) with
     | Prod (na,a,b) ->
 	let na',avoid = find_displayed_name_in all [] na ([],b) in
-	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
+	let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
 	!rigid, Array.to_list v
     | _ -> true, []
 
@@ -427,7 +427,7 @@ let compute_mib_implicits flags manual kn =
       (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
         (fun i mip ->
 	  (** No need to care about constraints here *)
-	  (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i))))
+	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i))))
         mib.mind_packets) in
   let env_ar = push_rel_context ar env in
   let imps_one_inductive i mip =
@@ -449,8 +449,8 @@ let compute_all_mib_implicits flags manual kn =
 
 let compute_var_implicits flags manual id =
   let env = Global.env () in
-  let (_,_,ty) = lookup_named id env in
-  compute_semi_auto_implicits env flags manual ty
+  let open Context.Named.Declaration in
+  compute_semi_auto_implicits env flags manual (get_type (lookup_named id env))
 
 (* Implicits of a global reference. *)
 
@@ -491,13 +491,15 @@ let implicits_of_global ref =
     let l = Refmap.find ref !implicits_table in
     try
       let rename_l = Arguments_renaming.arguments_names ref in
-      let rename imp name = match imp, name with
-       | Some (_, x,y), Name id -> Some (id, x,y)
-       | _ -> imp in
-      List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
+      let rec rename implicits names = match implicits, names with
+        | [], _ -> []
+        | _, [] -> implicits
+        | Some (_, x,y) :: implicits, Name id :: names ->
+           Some (id, x,y) :: rename implicits names
+        | imp :: implicits, _ :: names -> imp :: rename implicits names
+      in
+      List.map (fun (t, il) -> t, rename il rename_l) l
     with Not_found -> l
-    | Invalid_argument _ ->
-        anomaly (Pp.str "renamings list and implicits list have different lenghts")
   with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
@@ -525,12 +527,6 @@ let impls_of_context ctx =
   in
   List.rev_map map (List.filter is_set ctx)
 
-let section_segment_of_reference = function
-  | ConstRef con -> pi1 (section_segment_of_constant con)
-  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-    pi1 (section_segment_of_mutual_inductive kn)
-  | _ -> []
-
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
   | DefaultImpArgs -> DefaultImpArgs
@@ -544,7 +540,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
     (try
-      let vars = section_segment_of_reference ref in
+      let vars = variable_section_segment_of_reference ref in
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
       let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
@@ -562,7 +558,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplMutualInductive (kn,flags) ->
     (try
       let l' = List.map (fun (gr, l) ->
-	let vars = section_segment_of_reference gr in
+	let vars = variable_section_segment_of_reference gr in
 	let extra_impls = impls_of_context vars in
 	((if isVarRef gr then gr else pop_global_reference gr),
 	 List.map (add_section_impls vars extra_impls) l)) l
@@ -663,7 +659,7 @@ let check_inclusion l =
   let rec aux = function
     | n1::(n2::_ as nl) ->
 	if n1 <= n2 then
-	  error "Sequences of implicit arguments must be of different lengths";
+	  error "Sequences of implicit arguments must be of different lengths.";
 	aux nl
     | _ -> () in
   aux (List.map (fun (imps,_) -> List.length imps) l)