diff options
| author | sacerdot | 2004-09-29 13:28:08 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-29 13:28:08 +0000 |
| commit | 891178786f34efa1cff87e563ffa0596057f1f13 (patch) | |
| tree | a7ea1a284b00195032e3367bd454b234845f0684 | |
| parent | a3ebf0bc16223643a7cdf5da69b4c6a319bad73c (diff) | |
1. major code clean-up for the Prod case
2. cleaner behaviour: occurrences of the pattern in the type of a variable
bound by a dependent product are no longer
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6155 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/setoid_replace.ml | 25 |
1 files changed, 6 insertions, 19 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 77a5f21162..4045816eba 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1053,26 +1053,13 @@ let mark_occur gl t in_c input_relation input_direction = elim_duplicates identity (res_functions @ res_mors) | Prod (_, c1, c2) -> if (dependent (mkRel 1) c2) - then [ToKeep (in_c,output_relation,output_direction)] + then + errorlabstrm "Setoid_replace" + (str "Cannot rewrite in the type of a variable bound " ++ + str "in a dependent product.") else - (*CSC: output_relation in the two lines below is a bug. - I should use the two arguments of the relation associated to - coq_impl. Indeed all the Prod case is a bit hackerish. *) - let c1m = - aux output_relation (opposite_direction output_direction) c1 in - let c2m = - aux output_relation output_direction c2 - in - let a = cartesian_product [| c1m ; c2m |] in - List.fold_left - (fun res a -> - if get_mark a - then - (* this can be optimized since c1 and c2 will be *) - (* processed again *) - (aux output_relation output_direction - (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))) @ res - else (ToKeep (in_c,output_relation,output_direction))::res) [] a + aux output_relation output_direction + (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |])) | _ -> [ToKeep (in_c,output_relation,output_direction)] in let aux2 output_relation output_direction = |