Rewrite of the recursive defs handling in progress.

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

10 files changed, 181 insertions, 117 deletions

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 4cbfe90cf..fed61fb4c 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -43,7 +43,7 @@ open Eterm
 let require_library dirpath =
   let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
     Library.require_library [qualid] None
-
+(*
 let subtac_one_fixpoint env isevars (f, decl) = 
   let ((id, n, bl, typ, body), decl) = 
     Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) 
@@ -53,7 +53,7 @@ let subtac_one_fixpoint env isevars (f, decl) =
 	       Ppconstr.pr_constr_expr body)
     with _ -> ()
   in ((id, n, bl, typ, body), decl)
-    
+*)
 	      
 let subtac_fixpoint isevars l = 
   (* TODO: Copy command.build_recursive *)
diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli
index a0d2fb2b9..25922782c 100644
--- a/contrib/subtac/subtac.mli
+++ b/contrib/subtac/subtac.mli
@@ -1,14 +1,3 @@
 val require_library : string -> unit
-val subtac_one_fixpoint :
-  'a ->
-  'b ->
-  (Names.identifier * (int * Topconstr.recursion_order_expr) *
-   Topconstr.local_binder list * Topconstr.constr_expr *
-   Topconstr.constr_expr) *
-  'c ->
-  (Names.identifier * (int * Topconstr.recursion_order_expr) *
-   Topconstr.local_binder list * Topconstr.constr_expr *
-   Topconstr.constr_expr) *
-  'c
 val subtac_fixpoint : 'a -> 'b -> unit
 val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index f2a1a0185..70933e99b 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -106,25 +106,25 @@ module Coercion = struct
       : (Term.constr -> Term.constr) option 
       =
     let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
-      (try trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
+      (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++ 
 		  str " and "++ my_print_constr env y ++ 
 		  str " with evars: " ++ spc () ++
 		  my_print_evardefs !isevars);
        with _ -> ());
     let rec coerce_unify env x y =
-      (try trace (str "coerce_unify from " ++ (my_print_constr env x) ++ 
+      (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ 
 		  str " to "++ my_print_constr env y)
        with _ -> ());
       try 
 	isevars := the_conv_x_leq env x y !isevars;
-	(try (trace (str "Unified " ++ (my_print_constr env x) ++ 
-		     str " and "++ my_print_constr env y));
+	(try debug 1 (str "Unified " ++ (my_print_constr env x) ++ 
+			str " and "++ my_print_constr env y);
 	 with _ -> ());
 	None
       with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
     and coerce' env x y : (Term.constr -> Term.constr) option =
       let subco () = subset_coerce env isevars x y in
-	(try trace (str "coerce' from " ++ (my_print_constr env x) ++ 
+	(try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ 
 		    str " to "++ my_print_constr env y);
 	 with _ -> ());
 	match (kind_of_term x, kind_of_term y) with
@@ -370,7 +370,7 @@ module Coercion = struct
 
   let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
     (try
-       trace (str "inh_conv_coerce_to_fail called for " ++
+       debug 1 (str "inh_conv_coerce_to_fail called for " ++
 	      Termops.print_constr_env env t ++ str " and "++ spc () ++
 	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -436,7 +436,7 @@ module Coercion = struct
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
     (try 
-       trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++
+       debug 1 (str "Subtac_coercion.inh_conv_coerce_to called for " ++
 	      Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ 
 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -461,7 +461,7 @@ module Coercion = struct
 
   let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
     (try 
-       trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++
+       debug 1 (str "Subtac_coercion.inh_conv_coerces_to called for " ++
 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ 
 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b09228c06..10c5f580b 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -173,82 +173,146 @@ let list_of_local_binders l =
     | [] -> List.rev acc
   in aux [] l
 
-let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+let lift_binders k n l =
+  let rec aux n = function
+    | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+    | [] -> []
+  in aux n l
+
+let rec gen_rels = function
+    0 -> []
+  | n -> mkRel n :: gen_rels (pred n)
+
+let build_wellfounded (recname, n, bl,arityc,body) r notation boxed =
+  let sigma = Evd.empty in
+  let isevars = ref (Evd.create_evar_defs sigma) in
+  let env = Global.env() in 
+  let n = out_some n in 
+  let pr c = my_print_constr env c in
+  let prr = Printer.pr_rel_context env in
+  let pr_rel env = Printer.pr_rel_context env in
+  let _ = 
+    try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
+		 Ppconstr.pr_binders bl ++ str " : " ++ 
+		 Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+		 Ppconstr.pr_constr_expr body)
+    with _ -> ()
+  in
+  let env', binders_rel = interp_context isevars env bl in
+  let after, ((argname, _, argtyp) as arg), before = list_chop_hd (succ n) binders_rel in
+  let before_length, after_length = List.length before, List.length after in
+  let argid = match argname with Name n -> n | _ -> assert(false) in
+  let liftafter = lift_binders 1 after_length after in
+  let envwf = push_rel_context before env in
+  let wf_rel = interp_constr isevars envwf r in
+  let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in
+  let argid' = id_of_string (string_of_id argid ^ "'") in
+  let full_length = before_length + 1 + after_length in
+  let wfarg len = (Name argid', None, 
+		   mkSubset (Name argid') argtyp 
+		     (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
+  in
+  let top_bl = after @ (arg :: before) in
+  let intern_bl = after @ (wfarg 1 :: arg :: before) in
+  let top_env = push_rel_context top_bl env in
+  let intern_env = push_rel_context intern_bl env in
+  let top_arity = interp_type isevars top_env arityc in
+  (try debug 2 (str "Intern bl: " ++ prr intern_bl) with _ -> ());
+  let proj = (Lazy.force sig_).Coqlib.proj1 in
+  let projection = 
+    mkApp (proj, [| argtyp ;
+		    (mkLambda (Name argid', argtyp,
+			       (mkApp (wf_rel, [|mkRel 1; mkRel 2|])))) ;
+		    mkRel 1
+		 |])
+  in
+  (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
+  let intern_arity = substnl [projection] after_length top_arity in 
+  (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
+  let intern_arity_prod = it_mkProd_or_LetIn intern_arity intern_bl in
+  let intern_before_env = push_rel_context before env in
+  let intern_fun_bl = after @ [wfarg 1]  in
+  (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ());
+  let intern_fun_arity = intern_arity in
+  (try debug 2 (str "Intern fun arity: " ++ 
+		  my_print_constr intern_env intern_fun_arity) with _ -> ());
+  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
+  let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
+  let fun_bl = after @ (intern_fun_binder :: [arg]) in
+  (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ());
+  let fun_env = push_rel_context fun_bl intern_before_env in
+  let fun_arity = interp_type isevars fun_env arityc in
+  let intern_body = interp_casted_constr isevars fun_env body fun_arity in
+  let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
+  let _ = 
+      try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+		   str "Intern bl" ++ prr intern_bl ++ spc () ++
+		   str "Top bl" ++ prr top_bl ++ spc () ++
+		   str "Intern arity: " ++ pr intern_arity ++
+		   str "Top arity: " ++ pr top_arity ++ spc () ++
+		   str "Intern body " ++ pr intern_body_lam)
+      with _ -> ()
+  in
+  let impl = 
+    if Impargs.is_implicit_args()
+    then Impargs.compute_implicits top_env top_arity
+    else [] 
+  in
+  let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
+  let fix_def =
+    mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
+	  [| argtyp ;
+	     wf_rel ;
+	     make_existential dummy_loc intern_before_env isevars wf_proof ;
+	     prop ;
+	     intern_body_lam |])
+  in
+  let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
+  let def = it_mkLambda_or_LetIn def_appl binders_rel in
+  let typ = it_mkProd_or_LetIn top_arity binders_rel in
+    debug 2 (str "Constructed def");
+    debug 2 (my_print_constr intern_before_env def);
+    debug 2 (str "Type: " ++ my_print_constr env typ);
+  let fullcoqc = Evarutil.nf_isevar !isevars def in
+  let fullctyp = Evarutil.nf_isevar !isevars typ in
+  let _ = try trace (str "After evar normalization: " ++ spc () ++
+		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
+		 ++ str "Coq type: " ++ my_print_constr env fullctyp) 
+     with _ -> () 
+  in
+  let evm = non_instanciated_map env isevars in
+  let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in
+  let tac = Eterm.etermtac (evm, fullcoqc) in 
+    trace (str "Starting proof of goal: " ++ my_print_constr env fullctyp);
+    Command.start_proof recname goal_kind fullctyp (fun _ _ -> ());
+    trace (str "Started proof");
+    Pfedit.by tac
+    
+let build_mutrec l boxed =
   let sigma = Evd.empty
   and env0 = Global.env()
-  in 
+  in ()
+(*
   let lnameargsardef =
     (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
-      lnameargsardef
+    lnameargsardef
   in
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
   and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
   in
-  (* Build the recursive context and notations for the recursive types *)
+    (* Build the recursive context and notations for the recursive types *)
   let (rec_sign,rec_impls,arityl) = 
     List.fold_left 
-      (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) -> 
-	let isevars = ref (Evd.create_evar_defs sigma) in	  
-	  match ro with
-	      CStructRec ->
-		let arityc = Command.generalize_constr_expr arityc bl in
-		let arity = interp_type isevars env0 arityc in
-		let impl = 
-		  if Impargs.is_implicit_args()
-		  then Impargs.compute_implicits env0 arity
-		  else [] in
-		let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
-		  (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
-	    | CWfRec r -> 		    
-		let n = out_some n in 
-		let _ = 
-		  try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
-			     Ppconstr.pr_binders bl ++ str " : " ++ 
-			     Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
-			     Ppconstr.pr_constr_expr body)
-		  with _ -> ()
-		in
-		let env', binders_rel = interp_context isevars env0 bl in
-		let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
-		let argid = match argname with Name n -> n | _ -> assert(false) in
-		let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in
-		let envwf = push_rel_context before env0 in
-		let wf_rel = interp_constr isevars envwf r in
-		let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
-		let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in
-		let argid' = id_of_string (string_of_id argid ^ "'") in
-		let before_length, after_length = List.length before, List.length after in
-		let full_length = before_length + 1 + after_length in
-		let wfarg len = (Name argid, None, 
-				 mkSubset (Name argid') argtyp 
-				   (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
-		in
-		let new_bl = after' @ (accarg :: arg :: before)
-		and intern_bl =  after @ (wfarg (before_length + 1) :: before)
-		in
-		let intern_env = push_rel_context intern_bl env0 in
-		let env' = push_rel_context new_bl env0 in
-		let arity = interp_type isevars intern_env arityc in
-		let intern_arity = it_mkProd_or_LetIn arity intern_bl in
-		let arity' = interp_type isevars env' arityc in
-		let arity' = it_mkProd_or_LetIn arity' new_bl in
-		let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in
-		let _ = 
-		  let pr c = my_print_constr env c in
-		  let prr = Printer.pr_rel_context env in
-		    try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
-			       str "Intern bl" ++ prr intern_bl ++ spc () ++
-			       str "Extern bl" ++ prr new_bl ++ spc () ++
-			       str "Intern arity: " ++ pr intern_arity)
-		    with _ -> ()
-		in
-		let impl = 
-		  if Impargs.is_implicit_args()
-		  then Impargs.compute_implicits intern_env arity'
-		  else [] in
-		let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in
-		  (Environ.push_named (recname,None,arity') env, impls', 
-		   (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl))
+      (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) -> 
+	 let isevars = ref (Evd.create_evar_defs sigma) in	  
+	 let arityc = Command.generalize_constr_expr arityc bl in
+	 let arity = interp_type isevars env0 arityc in
+	 let impl = 
+	   if Impargs.is_implicit_args()
+	   then Impargs.compute_implicits env0 arity
+	   else [] in
+	 let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+	   (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
       (env0,[],[]) lnameargsardef in
   let arityl = List.rev arityl in
   let notations = 
@@ -430,6 +494,24 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 	     match cer with
 		 Environ.NoBody -> trace (str "Constant has no body")
 	       | Environ.Opaque -> trace (str "Constant is opaque")
-      )
+      )*)
+
+let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+  match lnameargsardef with
+    | ((id, (n, CWfRec r), bl, typ, body), no) :: [] -> 
+	(*let body = Subtac_utils.rewrite_cases env body in*)
+	  build_wellfounded (id, n, bl, typ, body) r no boxed
+    | l -> 
+	let lnameargsardef = 
+	  List.map (fun ((id, (n, ro), bl, typ, body), no) ->
+		 match ro with
+		     CStructRec -> (id, n, bl, typ, body), no
+		   | CWfRec _ -> 
+		       errorlabstrm "Subtac_command.build_recursive"
+			 (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
+	    lnameargsardef
+	in
+	  build_mutrec lnameargsardef boxed;
+	  assert(false)
       
       
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index e1bbbbb5b..90ffb8925 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -38,5 +38,6 @@ val interp_constr_judgment :
   constr_expr -> unsafe_judgment
 val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
 val recursive_message : global_reference array -> std_ppcmds
+
 val build_recursive :
   (fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 858fad1a8..bb35833f3 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -60,7 +60,7 @@ let pr_binder_list b =
 
 
 let rec rewrite_rec_calls l c = c
-
+(*
 let rewrite_fixpoint env l (f, decl) = 
   let (id, (n, ro), bl, typ, body) = f in
   let body = rewrite_rec_calls l body in
@@ -151,3 +151,4 @@ let rewrite_fixpoint env l (f, decl) =
 			 Ppconstr.pr_constr_expr body')
 	  in (id, (succ n, ro), bl', typ, body'), decl
 
+*)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index fafbb2da5..149e75807 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -15,14 +15,3 @@ val list_of_local_binders :
 val pr_binder_list :
   (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
 val rewrite_rec_calls : 'a -> 'b -> 'b
-val rewrite_fixpoint :
-  'a ->
-  'b ->
-  (Names.identifier * (int * Topconstr.recursion_order_expr) *
-   Topconstr.local_binder list * Topconstr.constr_expr *
-   Topconstr.constr_expr) *
-  'c ->
-  (Names.identifier * (int * Topconstr.recursion_order_expr) *
-   Topconstr.local_binder list * Topconstr.constr_expr *
-   Topconstr.constr_expr) *
-  'c
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 59c858a6a..31fea63d5 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -22,12 +22,14 @@ let fixsub = lazy (init_constant fixsub_module "Fix_sub")
 let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
 let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
 
-let make_ref s =  Qualid (dummy_loc, (qualid_of_string s))
-let well_founded_ref = make_ref "Init.Wf.Well_founded"
-let acc_ref = make_ref "Init.Wf.Acc"
-let acc_inv_ref = make_ref "Init.Wf.Acc_inv"
-let fix_sub_ref = make_ref "Coq.subtac.FixSub.Fix_sub"
-let lt_wf_ref = make_ref "Coq.Wf_nat.lt_wf"
+let make_ref l s = lazy (init_reference l s)
+let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
+let acc_ref = make_ref  ["Init";"Wf"] "Acc"
+let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
+let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
+let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
+
+let make_ref s = Qualid (dummy_loc, qualid_of_string s)
 let sig_ref = make_ref "Init.Specif.sig"
 let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
 let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
@@ -82,18 +84,19 @@ let my_print_evardefs = Evd.pr_evar_defs
 
 let my_print_tycon_type = Evarutil.pr_tycon_type
 
+let debug_level = 2
 
 let debug n s = 
-  if !Options.debug then
+  if !Options.debug && n >= debug_level then
     msgnl s
   else ()
 
 let debug_msg n s = 
-  if !Options.debug then s
+  if !Options.debug  && n >= debug_level then s
   else mt ()
 
 let trace s = 
-  if !Options.debug then msgnl s
+  if !Options.debug  && debug_level > 0 then msgnl s
   else ()
 
 let wf_relations = Hashtbl.create 10
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a90f281ff..4b25ff679 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -18,12 +18,11 @@ val fixsub_module : string list
 val init_constant : string list -> string -> constr
 val init_reference : string list -> string -> global_reference
 val fixsub : constr lazy_t
-val make_ref : string -> reference
-val well_founded_ref : reference
-val acc_ref : reference
-val acc_inv_ref : reference
-val fix_sub_ref : reference
-val lt_wf_ref : reference
+val well_founded_ref : global_reference lazy_t
+val acc_ref : global_reference lazy_t
+val acc_inv_ref : global_reference lazy_t
+val fix_sub_ref : global_reference lazy_t
+val lt_wf_ref : global_reference lazy_t
 val sig_ref : reference
 val proj1_sig_ref : reference
 val proj2_sig_ref : reference
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 481b6708d..ba5bdf232 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -12,8 +12,8 @@ reflexivity.
 Defined.
 
 Extraction testsig.
-Extraction sigS.
-Extract Inductive sigS => "" [ "" ].
+Extraction sig.
+Extract Inductive sig => "" [ "" ].
 Extraction testsig.
 
 Require Import Coq.Arith.Compare_dec.