Replacing "GenFixpoint" with "Function" and "mes" with "measure"

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

2 files changed, 8 insertions, 13 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 065eb17306..81527912dc 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -71,7 +71,7 @@ let compute_annot (name,annot,args,types,body) =
     | None ->
         if List.length names > 1 then
           user_err_loc
-            (dummy_loc,"GenFixpoint",
+            (dummy_loc,"Function",
              Pp.str "the recursive argument needs to be specified");
         let new_annot = (id_of_name (List.hd names)) in
 	(name,Struct new_annot,args,types,body)
@@ -329,8 +329,8 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 		     let names =  (Topconstr.names_of_local_assums args) in
 		     if  is_one_rec recdef  && List.length names > 1 then
 		       Util.user_err_loc
-			 (Util.dummy_loc,"GenFixpoint",
-			  Pp.str "the recursive argument needs to be specified in GenFixpoint")
+			 (Util.dummy_loc,"Function",
+			  Pp.str "the recursive argument needs to be specified in Function")
 		     else 
 		       (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 7b3d8cbda1..a238de895b 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -111,7 +111,7 @@ END
 VERNAC ARGUMENT EXTEND rec_annotation2
   [ "{"  "struct" ident(id)  "}"] -> [ Struct id ]
 | [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
-| [ "{" "mes" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ] 
+| [ "{" "measure" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ] 
 END
 
 
@@ -130,7 +130,7 @@ VERNAC ARGUMENT EXTEND rec_definition2
      let check_one_name () =
        if List.length names > 1 then
          Util.user_err_loc
-           (Util.dummy_loc,"GenFixpoint",
+           (Util.dummy_loc,"Function",
             Pp.str "the recursive argument needs to be specified");
      in
      let check_exists_args an =
@@ -138,7 +138,7 @@ VERNAC ARGUMENT EXTEND rec_definition2
 	 let id = match an with Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" in 
 	 (try ignore(Util.list_index (Name id) names - 1); annot
 	  with Not_found ->  Util.user_err_loc
-            (Util.dummy_loc,"GenFixpoint",
+            (Util.dummy_loc,"Function",
              Pp.str "No argument named " ++ Nameops.pr_id id)
 	 )
        with Failure "check_exists_args" ->  check_one_name ();annot
@@ -160,16 +160,11 @@ VERNAC ARGUMENT EXTEND rec_definitions2
 END
 
 
-VERNAC COMMAND EXTEND GenFixpoint
-   ["GenFixpoint" rec_definitions2(recsl)] ->
+VERNAC COMMAND EXTEND Function
+   ["Function" rec_definitions2(recsl)] ->
 	[ do_generate_principle false  recsl]
 END
 
-VERNAC COMMAND EXTEND IGenFixpoint
-   ["IGenFixpoint" rec_definitions2(recsl)] ->
-	[ do_generate_principle true  recsl]
-END
-
 
 VERNAC ARGUMENT EXTEND fun_scheme_arg
 | [ ident(princ_name) ":=" "Induction" "for" ident(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]