Remove dynamic stuff from constr_expr and glob_constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 3 insertions, 21 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8dfc201d7e..c88c666938 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -585,7 +585,6 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		let f_res = build_entry_lc env funnames args_res.to_avoid f in
 		combine_results combine_app f_res  args_res
-	    | GDynamic _ ->error "Not handled GDynamic"
 	    | GCast(_,b,_) ->
 		(* for an applied cast we just trash the cast part
 		   and restart the work.
@@ -698,7 +697,6 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
     | GRec _ -> error "Not handled GRec"
     | GCast(_,b,_) ->
 	build_entry_lc env funnames  avoid b
-    | GDynamic _ -> error "Not handled GDynamic"
 and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuples)
     (brl:Glob_term.cases_clauses) avoid :
@@ -1213,7 +1211,7 @@ let rec compute_cst_params relnames params = function
 		 discriminitation ones *)
   | GSort _ -> params
   | GHole _ -> params
-  | GIf _ | GRec _ | GCast _ | GDynamic _  ->
+  | GIf _ | GRec _ | GCast _ ->
       raise (UserError("compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0de1104e74..cdd0eaf715 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -183,7 +183,6 @@ let change_vars =
 	  GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
       | GCast(loc,b,CastCoerce) ->
 	  GCast(loc,change_vars mapping b,CastCoerce)
-      | GDynamic _ -> error "Not handled GDynamic"
   and change_vars_br mapping ((loc,idl,patl,res) as br) =
     let new_mapping = List.fold_right Idmap.remove idl mapping in
     if idmap_is_empty new_mapping
@@ -364,7 +363,6 @@ let rec alpha_rt excluded rt =
 	GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
     | GCast (loc,b,CastCoerce) ->
 	GCast(loc,alpha_rt excluded b,CastCoerce)
-    | GDynamic _ -> error "Not handled GDynamic"
     | GApp(loc,f,args) ->
 	GApp(loc,
 	     alpha_rt excluded f,
@@ -414,7 +412,6 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
     | GCast (_,b,CastCoerce) -> is_free_in b
-    | GDynamic _ -> raise (UserError("",str "Not handled GDynamic"))
   and is_free_in_br (_,ids,_,rt) =
     (not (List.mem id ids)) && is_free_in rt
   in
@@ -513,7 +510,6 @@ let replace_var_by_term x_id term =
 	  GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
       | GCast(loc,b,CastCoerce) ->
 	  GCast(loc,replace_var_by_pattern b,CastCoerce)
-      | GDynamic _ -> raise (UserError("",str "Not handled GDynamic"))
   and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
     if List.exists (fun id -> id_ord id x_id == 0) idl
     then br
@@ -604,7 +600,7 @@ let ids_of_glob_constr c =
       | GCases (loc,sty,rtntypopt,tml,brchl) ->
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
       | GRec _ -> failwith "Fix inside a constructor branch"
-      | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> []
+      | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
   in
   (* build the set *)
   List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c)
@@ -668,7 +664,6 @@ let zeta_normalize =
 	  GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
       | GCast(loc,b,CastCoerce) ->
 	  GCast(loc,zeta_normalize_term b,CastCoerce)
-      | GDynamic _ -> raise (UserError("",str "Not handled GDynamic"))
   and zeta_normalize_br (loc,idl,patl,res) =
     (loc,idl,patl,zeta_normalize_term res)
   in
@@ -706,7 +701,6 @@ let expand_as =
 	  GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
       | GRec _ ->  error "Not handled GRec"
-      | GDynamic _ -> error "Not handled GDynamic"
       | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t))
       | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce)
       | GCases(loc,sty,po,el,brl) ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1ce6564c1c..8caeca57ab 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -189,7 +189,7 @@ let rec is_rec names =
   let check_id id names =  Idset.mem id names in
   let rec lookup names = function
     | GVar(_,id) -> check_id id names
-    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ | GDynamic _ -> false
+    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
     | GCast(_,b,_) -> lookup names b
     | GRec _ -> error "GRec not handled"
     | GIf(_,b,_,lhs,rhs) ->
@@ -764,7 +764,6 @@ let rec add_args id new_args b =
   | CGeneralization _ -> anomaly "add_args : CGeneralization"
   | CPrim _ -> b
   | CDelimiters _ -> anomaly "add_args : CDelimiters"
-  | CDynamic _ -> anomaly "add_args : CDynamic"
 exception Stop of  Topconstr.constr_expr
 
 
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index a842f36eba..d300a71ccc 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -558,15 +558,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	in
 	  inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-    | GDynamic (loc,d) ->
-	if (Dyn.tag d) = "constr" then
-	  let c = constr_out d in
-	  let j = (Retyping.get_judgment_of env !evdref c) in
-	    j
-	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
-	else
-	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))
-
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
   and pretype_type valcon env evdref lvar = function
     | GHole loc ->