Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation

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

6 files changed, 22 insertions, 37 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 353fe51986..aaf9637f87 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -80,7 +80,7 @@ val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
 
 (* Exported for program.ml only *)
 val clenv_add_sign : 
-  (identifier * typed_type) -> wc clausenv -> wc clausenv
+  (identifier * types) -> wc clausenv -> wc clausenv
 val constrain_clenv_to_subterm : 
   wc clausenv -> constr * constr -> wc clausenv * constr
 val clenv_constrain_dep_args_of : 
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index b1c4a5a2c8..ac6bc06301 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -41,7 +41,7 @@ val w_Underlying : walking_constraints -> enamed_declarations
 val w_env        : walking_constraints -> env
 val w_hyps       : walking_constraints -> named_context
 val w_type_of    : walking_constraints -> constr -> constr
-val w_add_sign   : (identifier * typed_type) -> walking_constraints 
+val w_add_sign   : (identifier * types) -> walking_constraints 
                      -> walking_constraints
 
 val w_IDTAC      : w_tactic
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 61126b262f..2bf95aed11 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -255,7 +255,7 @@ let convert_hyp env sigma id ty =
     (fun env (idc,c,ct) _ ->
        if !check && not (is_conv env sigma ty (body_of_type ct)) then
 	 error "convert-hyp rule passed non-converting term";
-       push_named_decl (idc,c,get_assumption_of env sigma ty) env)
+       push_named_decl (idc,c,ty) env)
 
 let replace_hyp env id d =
   apply_to_hyp env id
@@ -291,16 +291,14 @@ let prim_refiner r sigma goal =
         (match kind_of_term (strip_outer_cast cl) with
 	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma c1
-	       and v = mkVar id in
-	       let sg = mk_goal info (push_named_assum (id,a) env) (subst1 v b) in
+	       let sg = mk_goal info (push_named_assum (id,c1) env)
+			  (subst1 (mkVar id) b) in
 	       [sg]
 	   | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma t1
-	       and v = mkVar id in
 	       let sg =
-		 mk_goal info (push_named_def (id,c1,a) env) (subst1 v b) in
+		 mk_goal info (push_named_def (id,c1,t1) env)
+		   (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
 	       if !check then raise (RefinerError IntroNeedsProduct)
@@ -312,17 +310,13 @@ let prim_refiner r sigma goal =
         (match kind_of_term (strip_outer_cast cl) with
 	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma c1
-	       and v = mkVar id in
-	       let env' = insert_after_hyp env whereid (id,None,a) in
-	       let sg = mk_goal info env' (subst1 v b) in 
+	       let env' = insert_after_hyp env whereid (id,None,c1) in
+	       let sg = mk_goal info env' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma t1
-	       and v = mkVar id in
-	       let env' = insert_after_hyp env whereid (id,Some c1,a) in
-	       let sg = mk_goal info env' (subst1 v b) in 
+	       let env' = insert_after_hyp env whereid (id,Some c1,t1) in
+	       let sg = mk_goal info env' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -332,17 +326,13 @@ let prim_refiner r sigma goal =
 	(match kind_of_term (strip_outer_cast cl) with
            | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma c1
-	       and v = mkVar id in
-	       let env' = replace_hyp env id (id,None,a) in
-	       let sg = mk_goal info env' (subst1 v b) in
+	       let env' = replace_hyp env id (id,None,c1) in
+	       let sg = mk_goal info env' (subst1 (mkVar id) b) in
 	       [sg]
            | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma t1
-	       and v = mkVar id in
-	       let env' = replace_hyp env id (id,Some c1,a) in
-	       let sg = mk_goal info env' (subst1 v b) in
+	       let env' = replace_hyp env id (id,Some c1,t1) in
+	       let sg = mk_goal info env' (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -365,8 +355,7 @@ let prim_refiner r sigma goal =
      	check_ind n cl;
 	if !check && mem_named_context f sign then
 	  error ("The name "^(string_of_id f)^" is already used");
-        let a = get_assumption_of env sigma cl in
-        let sg = mk_goal info (push_named_assum (f,a) env) cl in
+        let sg = mk_goal info (push_named_assum (f,cl) env) cl in
         [sg]
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
@@ -392,8 +381,7 @@ let prim_refiner r sigma goal =
 		       "mutual inductive declaration");
 	      if mem_named_context f sign then 
 		error "name already used in the environment";
-	      let a = get_assumption_of env sigma ar in
-	      mk_sign (add_named_assum (f,a) sign) (lar',lf',ln')
+	      mk_sign (add_named_assum (f,ar) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
 	      List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
@@ -419,9 +407,7 @@ let prim_refiner r sigma goal =
                 (let _ = lookup_named f env in
                 error "name already used in the environment")
               with
-              |	Not_found ->
-  	        let a = get_assumption_of env sigma ar in
-	        mk_env (push_named_assum (f,a) env) (lar',lf'))
+              |	Not_found -> mk_env (push_named_assum (f,ar) env) (lar',lf'))
 	  | ([],[]) -> List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 868e71f850..495a9ca826 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -255,9 +255,8 @@ let extract_open_proof sigma pf =
 	       mkNamedProd_or_LetIn (id,c,ty) concl)
             sorted_rels goal.evar_concl
 	in
-	let ass = Retyping.get_assumption_of goal.evar_env sigma abs_concl in
 	let mv = new_meta() in
-	open_obligations := (mv,ass):: !open_obligations;
+	open_obligations := (mv,abs_concl):: !open_obligations;
 	applist (mkMeta mv, List.map (fun (n,_) -> mkRel n) sorted_rels) 
 	  
     | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 4c1e2f9770..47d44a9f19 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -117,7 +117,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate
 val weak_undo_pftreestate : pftreestate -> pftreestate
 
 val mk_pftreestate : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list
+val extract_open_pftreestate : pftreestate -> constr * (int * types) list
 val extract_pftreestate : pftreestate -> constr
 val first_unproven : pftreestate -> pftreestate
 val last_unproven : pftreestate -> pftreestate
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 8eb0b39e6a..717c5212f3 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -98,7 +98,7 @@ val weak_undo_pftreestate   : pftreestate -> pftreestate
 val solve_nth_pftreestate   : int -> tactic -> pftreestate -> pftreestate
 val solve_pftreestate       : tactic -> pftreestate -> pftreestate
 val mk_pftreestate          : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list
+val extract_open_pftreestate : pftreestate -> constr * (int * types) list
 val extract_pftreestate     : pftreestate -> constr
 val first_unproven          : pftreestate -> pftreestate
 val last_unproven           : pftreestate -> pftreestate
@@ -197,7 +197,7 @@ val w_Underlying        : walking_constraints -> enamed_declarations
 val w_env               : walking_constraints -> env
 val w_hyps              : walking_constraints -> named_context
 val w_type_of           : walking_constraints -> constr -> constr
-val w_add_sign          : (identifier * typed_type) 
+val w_add_sign          : (identifier * types) 
                           -> walking_constraints -> walking_constraints
 val w_IDTAC             : w_tactic
 val w_ORELSE            : w_tactic -> w_tactic -> w_tactic