Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg

1 files changed, 41 insertions, 29 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b161d001..1dd735ad 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -166,6 +166,8 @@ let error_inductive_parameter_not_implicit loc =
 (* Pre-computing the implicit arguments and arguments scopes needed   *)
 (* for interpretation *)
 
+let parsing_explicit = ref false
+
 let empty_internalization_env = Idmap.empty
 
 let compute_explicitable_implicit imps = function
@@ -408,12 +410,12 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b
   | LocalRawAssum(nal,bk,ty) ->
       (match bk with
       | Default k ->
-          let (loc,na) = List.hd nal in
-	  (* TODO: fail if several names with different implicit types *)
-	  let ty = locate_if_isevar loc na (intern_type env ty) in
+	  let ty = intern_type env ty in
+          let impls = impls_type_list ty in
 	    List.fold_left
-	     (fun (env,bl) na ->
-	       (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
+	     (fun (env,bl) (loc,na as locna) ->
+	       (push_name_env lvar impls env locna,
+                (na,k,None,locate_if_isevar loc na ty)::bl))
 	      (env,bl) nal
       | Generalized (b,b',t) ->
 	  let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in
@@ -452,12 +454,12 @@ let iterate_binder intern lvar (env,bl) = function
       let intern_type env = intern (set_type_scope env) in
       (match bk with
       | Default k ->
-          let (loc,na) = List.hd nal in
-	  (* TODO: fail if several names with different implicit types *)
 	  let ty = intern_type env ty in
-	  let ty = locate_if_isevar loc na ty in
+          let impls = impls_type_list ty in
 	  List.fold_left
-	    (fun (env,bl) na -> (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
+	    (fun (env,bl) (loc,na as locna) ->
+              (push_name_env lvar impls env locna,
+               (na,k,None,locate_if_isevar loc na ty)::bl))
 	    (env,bl) nal
       | Generalized (b,b',t) ->
 	  let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
@@ -731,8 +733,9 @@ let apply_scope_env env = function
   | [] -> {env with tmp_scope = None}, []
   | sc::scl -> {env with tmp_scope = sc}, scl
 
-let rec simple_adjust_scopes n = function
-  | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
+let rec simple_adjust_scopes n scopes =
+  if n=0 then [] else match scopes with
+  | [] -> None :: simple_adjust_scopes (n-1) []
   | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
 
 let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
@@ -809,9 +812,6 @@ let message_redundant_alias (id1,id2) =
 
 (* Expanding notations *)
 
-let error_invalid_pattern_notation loc =
-  user_err_loc (loc,"",str "Invalid notation for pattern.")
-
 let chop_aconstr_constructor loc (ind,k) args =
   if List.length args = 0 then (* Tolerance for a @id notation *) args else
     begin
@@ -1293,7 +1293,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
                 find_appl_head_data c, args
             | x -> (intern env f,[],[],[]), args in
 	let args =
-	  intern_impargs c env impargs args_scopes (merge_impargs l args) in
+          intern_impargs c env impargs args_scopes (merge_impargs l args) in
 	check_projection isproj (List.length args) c;
 	(match c with
           (* Now compact "(f args') args" *)
@@ -1417,13 +1417,16 @@ let internalize sigma globalenv env allow_patvar lvar c =
     (tm',(snd na,typ)), na::ids
 
   and iterate_prod loc2 env bk ty body nal =
-    let rec default env bk = function
-    | (loc1,na as locna)::nal ->
-	if nal <> [] then check_capture loc1 ty na;
-	let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
-	  GProd (join_loc loc1 loc2, na, bk, ty, body)
-    | [] -> intern_type env body
+    let default env bk = function
+    | (loc1,na)::nal' as nal ->
+	if nal' <> [] then check_capture loc1 ty na;
+        let ty = intern_type env ty in
+        let impls = impls_type_list ty in
+	let env = List.fold_left (push_name_env lvar impls) env nal in
+        List.fold_right (fun (loc,na) c ->
+          GProd (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c))
+          nal (intern_type env body)
+    | [] -> assert false
     in
       match bk with
 	| Default b -> default env b nal
@@ -1433,13 +1436,16 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	      it_mkGProd ibind body
 
   and iterate_lam loc2 env bk ty body nal =
-    let rec default env bk = function
-      | (loc1,na as locna)::nal ->
-	  if nal <> [] then check_capture loc1 ty na;
-	  let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	  let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
-	    GLambda (join_loc loc1 loc2, na, bk, ty, body)
-      | [] -> intern env body
+    let default env bk = function
+    | (loc1,na)::nal' as nal ->
+        if nal' <> [] then check_capture loc1 ty na;
+        let ty = intern_type env ty in
+        let impls = impls_type_list ty in
+	let env = List.fold_left (push_name_env lvar impls) env nal in
+        List.fold_right (fun (loc,na) c ->
+          GLambda (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c))
+          nal (intern env body)
+    | [] -> assert false
     in match bk with
       | Default b -> default env b nal
       | Generalized (b, b', t) ->
@@ -1450,6 +1456,12 @@ let internalize sigma globalenv env allow_patvar lvar c =
   and intern_impargs c env l subscopes args =
     let l = select_impargs_size (List.length args) l in
     let eargs, rargs = extract_explicit_arg l args in
+    if !parsing_explicit then
+      if eargs <> [] then
+        error "Arguments given by name or position not supported in explicit mode."
+      else
+        intern_args env subscopes rargs
+    else
     let rec aux n impl subscopes eargs rargs =
       let (enva,subscopes') = apply_scope_env env subscopes in
       match (impl,rargs) with